def GRConstruction.rel (M : Type u) [CommMonoid M] : M × M → M × M → Prop

Equations

• GRConstruction.rel M (x_2, y) (x', y') = ∃ (z : M), x_2 * y' * z = x' * y * z

def AddGRConstruction.rel (M : Type u) [AddCommMonoid M] : M × M → M × M → Prop

Equations

• AddGRConstruction.rel M (x_2, y) (x', y') = ∃ (z : M), x_2 + y' + z = x' + y + z

theorem GRConstruction.rel_refl (M : Type u) [CommMonoid M] (x : M × M) : GRConstruction.rel M x x

theorem AddGRConstruction.rel_refl (M : Type u) [AddCommMonoid M] (x : M × M) : AddGRConstruction.rel M x x

theorem GRConstruction.rel_symm (M : Type u) [CommMonoid M] {x y : M × M} : GRConstruction.rel M x y → GRConstruction.rel M y x

theorem AddGRConstruction.rel_symm (M : Type u) [AddCommMonoid M] {x y : M × M} : AddGRConstruction.rel M x y → AddGRConstruction.rel M y x

theorem GRConstruction.rel_trans (M : Type u) [CommMonoid M] {x y z : M × M} : GRConstruction.rel M x y → GRConstruction.rel M y z → GRConstruction.rel M x z

theorem AddGRConstruction.rel_trans (M : Type u) [AddCommMonoid M] {x y z : M × M} : AddGRConstruction.rel M x y → AddGRConstruction.rel M y z → AddGRConstruction.rel M x z

def GRConstruction.con (M : Type u) [CommMonoid M] : Con (M × M)

Equations

• GRConstruction.con M = { r := GRConstruction.rel M, iseqv := ⋯, mul' := ⋯ }

def AddGRConstruction.addCon (M : Type u) [AddCommMonoid M] : AddCon (M × M)

Equations

• AddGRConstruction.addCon M = { r := AddGRConstruction.rel M, iseqv := ⋯, add' := ⋯ }

@[simp]

theorem GRConstruction.con_r (M : Type u) [CommMonoid M] (a✝ a✝¹ : M × M) : (GRConstruction.con M).toSetoid a✝ a✝¹ = GRConstruction.rel M a✝ a✝¹

@[simp]

theorem AddGRConstruction.addCon_r (M : Type u) [AddCommMonoid M] (a✝ a✝¹ : M × M) : (AddGRConstruction.addCon M).toSetoid a✝ a✝¹ = AddGRConstruction.rel M a✝ a✝¹

theorem GRConstruction.con_def (M : Type u) [CommMonoid M] (x y : M × M) : (GRConstruction.con M) x y = ∃ (z : M), x.1 * y.2 * z = y.1 * x.2 * z

theorem AddGRConstruction.con_def (M : Type u) [AddCommMonoid M] (x y : M × M) : (AddGRConstruction.addCon M) x y = ∃ (z : M), x.1 + y.2 + z = y.1 + x.2 + z

@[reducible, inline]

abbrev GR (M : Type u_1) [CommMonoid M] : Type u_1

Equations

• GR M = (GRConstruction.con M).Quotient

@[reducible, inline]

abbrev AddGR (M : Type u_1) [AddCommMonoid M] : Type u_1

Equations

• AddGR M = (AddGRConstruction.addCon M).Quotient

def GR.«term_ᵍʳ» : Lean.TrailingParserDescr

Equations

• GR.«term_ᵍʳ» = Lean.ParserDescr.trailingNode `GR.«term_ᵍʳ» 1024 1024 (Lean.ParserDescr.symbol "ᵍʳ")

def GR.«term_ᵃᵍʳ» : Lean.TrailingParserDescr

Equations

• GR.«term_ᵃᵍʳ» = Lean.ParserDescr.trailingNode `GR.«term_ᵃᵍʳ» 1024 1024 (Lean.ParserDescr.symbol "ᵃᵍʳ")

def GR.emb (M : Type u) [CommMonoid M] : M →* GR M

Equations

• GR.emb M = { toFun := fun (x : M) => ↑(x, 1), map_one' := ⋯, map_mul' := ⋯ }

def AddGR.emb (M : Type u) [AddCommMonoid M] : M →+ AddGR M

Equations

• AddGR.emb M = { toFun := fun (x : M) => ↑(x, 0), map_zero' := ⋯, map_add' := ⋯ }

theorem GR.emb_injective (M : Type u) [CommMonoid M] [IsCancelMul M] : Function.Injective ⇑(GR.emb M)

theorem AddGR.emb_injective (M : Type u) [AddCommMonoid M] [IsCancelAdd M] : Function.Injective ⇑(AddGR.emb M)

theorem GR.recOn {M : Type u} [CommMonoid M] {motive : GR M → Prop} (x : GR M) (base : ∀ (x : M), motive ↑(x, 1)) (inv : ∀ (x : M), motive ↑(1, x)) (mul : ∀ (x y : GR M), motive x → motive y → motive (x * y)) : motive x

theorem AddGR.recOn {M : Type u} [AddCommMonoid M] {motive : AddGR M → Prop} (x : AddGR M) (base : ∀ (x : M), motive ↑(x, 0)) (inv : ∀ (x : M), motive ↑(0, x)) (mul : ∀ (x y : AddGR M), motive x → motive y → motive (x + y)) : motive x

instance GR.instInv {M : Type u} [CommMonoid M] : Inv (GR M)

Equations

• GR.instInv = { inv := ⇑((GRConstruction.con M).lift ((GRConstruction.con M).mk'.comp { toFun := Prod.swap, map_one' := ⋯, map_mul' := ⋯ }) ⋯) }

instance AddGR.instNeg {M : Type u} [AddCommMonoid M] : Neg (AddGR M)

Equations

• AddGR.instNeg = { neg := ⇑((AddGRConstruction.addCon M).lift ((AddGRConstruction.addCon M).mk'.comp { toFun := Prod.swap, map_zero' := ⋯, map_add' := ⋯ }) ⋯) }

@[simp]

theorem GR.inv_coe {M : Type u} [CommMonoid M] (x y : M) : (↑(x, y))⁻¹ = ↑(y, x)

@[simp]

theorem AddGR.neg_coe {M : Type u} [AddCommMonoid M] (x y : M) : -↑(x, y) = ↑(y, x)

@[simp]

theorem GR.coe_same {M : Type u} [CommMonoid M] (x : M) : ↑(x, x) = 1

@[simp]

theorem AddGR.coe_same {M : Type u} [AddCommMonoid M] (x : M) : ↑(x, x) = 0

instance GR.instGroup {M : Type u} [CommMonoid M] : Group (GR M)

Equations

• GR.instGroup = Group.mk ⋯

instance AddGR.instAddGroup {M : Type u} [AddCommMonoid M] : AddGroup (AddGR M)

Equations

• AddGR.instAddGroup = AddGroup.mk ⋯

def GR.lift {M : Type u} [CommMonoid M] {G : Type v} [Group G] (f : M →* G) : GR M →* G

Equations

• GR.lift f = (GRConstruction.con M).lift { toFun := fun (p : M × M) => f p.1 * (f p.2)⁻¹, map_one' := ⋯, map_mul' := ⋯ } ⋯

def AddGR.lift {M : Type u} [AddCommMonoid M] {G : Type v} [AddGroup G] (f : M →+ G) : AddGR M →+ G

Equations

• AddGR.lift f = (AddGRConstruction.addCon M).lift { toFun := fun (p : M × M) => f p.1 + -f p.2, map_zero' := ⋯, map_add' := ⋯ } ⋯

@[simp]

theorem GR.lift_comp_emb {M : Type u} [CommMonoid M] {G : Type v} [Group G] (f : M →* G) : (GR.lift f).comp (GR.emb M) = f

@[simp]

theorem AddGR.lift_comp_emb {M : Type u} [AddCommMonoid M] {G : Type v} [AddGroup G] (f : M →+ G) : (AddGR.lift f).comp (AddGR.emb M) = f

@[simp]

theorem GR.lift_emb_apply {M : Type u} [CommMonoid M] {G : Type v} [Group G] (f : M →* G) (x : M) : (GR.lift f) ((GR.emb M) x) = f x

@[simp]

theorem AddGR.lift_emb_apply {M : Type u} [AddCommMonoid M] {G : Type v} [AddGroup G] (f : M →+ G) (x : M) : (AddGR.lift f) ((AddGR.emb M) x) = f x

@[simp]

theorem GR.lift_uniq {M : Type u} [CommMonoid M] {G : Type v} [Group G] (f : M →* G) (f' : GR M →* G) (h : f'.comp (GR.emb M) = f) : f' = GR.lift f

@[simp]

theorem AddGR.lift_uniq {M : Type u} [AddCommMonoid M] {G : Type v} [AddGroup G] (f : M →+ G) (f' : AddGR M →+ G) (h : f'.comp (AddGR.emb M) = f) : f' = AddGR.lift f

@[simp]

theorem GR.lift_apply_coe {M : Type u} [CommMonoid M] {G : Type v} [Group G] (f : M →* G) (a b : M) : (GR.lift f) ↑(a, b) = f a * (f b)⁻¹

@[simp]

theorem AddGR.lift_apply_coe {M : Type u} [AddCommMonoid M] {G : Type v} [AddGroup G] (f : M →+ G) (a b : M) : (AddGR.lift f) ↑(a, b) = f a + -f b

instance GR.instIsCancelMulSubtypeMemSubmonoid {M : Type u} [CommGroup M] (N : Submonoid M) : IsCancelMul ↥N

noncomputable def GR.equivAsSubgroup {M : Type u} [CommGroup M] (N : Submonoid M) : GR ↥N ≃* ↥(Subgroup.closure ↑N)

Equations

• GR.equivAsSubgroup N = MulEquiv.ofBijective (GR.lift (Submonoid.inclusion ⋯)) ⋯

noncomputable def AddGR.equivAsAddSubgroup {M : Type u} [AddCommGroup M] (N : AddSubmonoid M) : AddGR ↥N ≃+ ↥(AddSubgroup.closure ↑N)

Equations

• AddGR.equivAsAddSubgroup N = AddEquiv.ofBijective (AddGR.lift (AddSubmonoid.inclusion ⋯)) ⋯

@[simp]

theorem AddGR.equivAsAddSubgroup_apply {M : Type u} [AddCommGroup M] (N : AddSubmonoid M) (a : AddGR ↥N) : (AddGR.equivAsAddSubgroup N) a = (AddGR.lift (AddSubmonoid.inclusion ⋯)) a

@[simp]

theorem GR.equivAsSubgroup_apply {M : Type u} [CommGroup M] (N : Submonoid M) (a : GR ↥N) : (GR.equivAsSubgroup N) a = (GR.lift (Submonoid.inclusion ⋯)) a