This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Mathlib.Tactic | |
inductive E | |
| lit : Bool → E | |
| var : Nat → E | |
| ite : E → E → E → E | |
deriving DecidableEq | |
def E.hasNestedIf : E → Bool | |
| lit _ => false |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open Monoid Monoid.Coprod SemidirectProduct | |
-- def Monoid.CoprodI.mapEquivHom (ι M : Type*) [Monoid M] : | |
-- Equiv.Perm ι →* MulAut (Monoid.CoprodI (fun _ : ι => M)) := | |
-- { toFun := fun e => | |
-- MonoidHom.toMulEquiv | |
-- (Monoid.CoprodI.lift (fun i => | |
-- CoprodI.of (M := fun _ : ι => M) (i := e i))) | |
-- (Monoid.CoprodI.lift (fun i => | |
-- CoprodI.of (M := fun _ : ι => M) (i := e.symm i))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Mathlib.GroupTheory.SemidirectProduct | |
import Mathlib.GroupTheory.FreeGroup | |
open FreeGroup SemidirectProduct Multiplicative | |
def freeAction : Multiplicative ℤ →* MulAut (FreeGroup (Multiplicative ℤ)) := | |
zpowersHom _ (freeGroupCongr (MulAction.toPermHom (Multiplicative ℤ) | |
(Multiplicative ℤ) (ofAdd 1))) | |
#print mint | |
example : FreeGroup Bool ≃* |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import order.zorn | |
import category_theory.category.preorder | |
import category_theory.limits.cones | |
universes u v w | |
namespace category_theory | |
open limits |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
inductive AccT {α : Type u} (r : α → α → Sort v) : α → Type (max u v) where | |
| intro (x : α) (h : (y : α) → r y x → AccT r y) : AccT r x | |
namespace AccT | |
def inv {x y : α} : (h₁ : AccT r x) → (h₂ : r y x) → AccT r y | |
| ⟨_, h⟩, h₂ => h y h₂ | |
def NatAccT : (n : Nat) → @AccT Nat (. < .) n | |
| 0 => AccT.intro 0 (fun y h => (Nat.not_lt_zero y h).elim) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
universe u | |
inductive EQ {α : Type u} (a : α) : α → Type | |
| refl : EQ a | |
def casT {α β : Type} (h : EQ α β) (a : α) : β := | |
@EQ.rec_on Type α (λ A hA, A) β h a | |
def EQ.trans {α : Type u} {a b c : α} (h₁ : EQ a b) (h₂ : EQ b c) : EQ a c := | |
@EQ.rec_on α b (λ A hA, EQ a A) c h₂ h₁ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import data.mv_polynomial.variables | |
import field_theory.is_alg_closed.basic | |
import data.finset.lattice | |
import data.zmod.basic | |
noncomputable theory | |
/-- the data of a polynomial map consists of n polynomials in n variables -/ | |
@[simp] def poly_map (K : Type*) [comm_semiring K] (n : ℕ) : Type* := | |
fin n → mv_polynomial (fin n) K |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import tactic | |
variables (P : Type) [partial_order P] | |
def presheaf : Type := | |
{ s : P → Prop // ∀ a b, a ≤ b → s b → s a } | |
instance : has_coe_to_fun (presheaf P) (λ _, P → Prop) := | |
⟨subtype.val⟩ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import linear_algebra.finsupp | |
variables {R α M N P : Type} [comm_ring R] [add_comm_group M] [module R M] | |
variables [add_comm_group N] [module R N] | |
variables [add_comm_group P] [module R P] | |
noncomputable theory | |
namespace poly_example |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import data.set.function | |
import data.fintype.basic | |
import data.finset.basic | |
import data.fin | |
import tactic | |
open finset function | |
@[derive fintype, derive decidable_eq] | |
structure cell := (r : fin 9) (c : fin 9) |
NewerOlder