Skip to content

Instantly share code, notes, and snippets.

View ChrisHughes24's full-sized avatar

Chris Hughes ChrisHughes24

View GitHub Profile
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
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)))
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 ≃*
import order.zorn
import category_theory.category.preorder
import category_theory.limits.cones
universes u v w
namespace category_theory
open limits
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)
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₁
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
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⟩
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
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)