HepLean Documentation

Mathlib.Algebra.Group.Ext

Extensionality lemmas for monoid and group structures #

In this file we prove extensionality lemmas for Monoid and higher algebraic structures with one binary operation. Extensionality lemmas for structures that are lower in the hierarchy can be found in Algebra.Group.Defs.

Implementation details #

To get equality of npow etc, we define a monoid homomorphism between two monoid structures on the same type, then apply lemmas like MonoidHom.map_div, MonoidHom.map_pow etc.

To refer to the * operator of a particular instance i, we use (letI := i; HMul.hMul : M → M → M) instead of i.mul (which elaborates to Mul.mul), as the former uses HMul.hMul which is the canonical spelling.

Tags #

monoid, group, extensionality

theorem AddMonoid.ext {M : Type u} ⦃m₁ : AddMonoid M⦄ ⦃m₂ : AddMonoid M⦄ (h_mul : HAdd.hAdd = HAdd.hAdd) :

m₁ = m₂

theorem Monoid.ext_iff {M : Type u} {m₁ : Monoid M} {m₂ : Monoid M} :

m₁ = m₂ ↔ HMul.hMul = HMul.hMul

theorem AddMonoid.ext_iff {M : Type u} {m₁ : AddMonoid M} {m₂ : AddMonoid M} :

m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd

theorem Monoid.ext {M : Type u} ⦃m₁ : Monoid M⦄ ⦃m₂ : Monoid M⦄ (h_mul : HMul.hMul = HMul.hMul) :

m₁ = m₂

theorem AddCommMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@AddCommMonoid.toAddMonoid M)

theorem CommMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@CommMonoid.toMonoid M)

theorem AddCommMonoid.ext {M : Type u_1} ⦃m₁ : AddCommMonoid M⦄ ⦃m₂ : AddCommMonoid M⦄ (h_mul : HAdd.hAdd = HAdd.hAdd) :

m₁ = m₂

theorem CommMonoid.ext_iff {M : Type u_1} {m₁ : CommMonoid M} {m₂ : CommMonoid M} :

m₁ = m₂ ↔ HMul.hMul = HMul.hMul

theorem AddCommMonoid.ext_iff {M : Type u_1} {m₁ : AddCommMonoid M} {m₂ : AddCommMonoid M} :

m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd

theorem CommMonoid.ext {M : Type u_1} ⦃m₁ : CommMonoid M⦄ ⦃m₂ : CommMonoid M⦄ (h_mul : HMul.hMul = HMul.hMul) :

m₁ = m₂

theorem AddLeftCancelMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@AddLeftCancelMonoid.toAddMonoid M)

theorem LeftCancelMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@LeftCancelMonoid.toMonoid M)

theorem AddLeftCancelMonoid.ext {M : Type u} ⦃m₁ : AddLeftCancelMonoid M⦄ ⦃m₂ : AddLeftCancelMonoid M⦄ (h_mul : HAdd.hAdd = HAdd.hAdd) :

m₁ = m₂

theorem AddLeftCancelMonoid.ext_iff {M : Type u} {m₁ : AddLeftCancelMonoid M} {m₂ : AddLeftCancelMonoid M} :

m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd

theorem LeftCancelMonoid.ext_iff {M : Type u} {m₁ : LeftCancelMonoid M} {m₂ : LeftCancelMonoid M} :

m₁ = m₂ ↔ HMul.hMul = HMul.hMul

theorem LeftCancelMonoid.ext {M : Type u} ⦃m₁ : LeftCancelMonoid M⦄ ⦃m₂ : LeftCancelMonoid M⦄ (h_mul : HMul.hMul = HMul.hMul) :

m₁ = m₂

theorem AddRightCancelMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@AddRightCancelMonoid.toAddMonoid M)

theorem RightCancelMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@RightCancelMonoid.toMonoid M)

theorem AddRightCancelMonoid.ext {M : Type u} ⦃m₁ : AddRightCancelMonoid M⦄ ⦃m₂ : AddRightCancelMonoid M⦄ (h_mul : HAdd.hAdd = HAdd.hAdd) :

m₁ = m₂

theorem AddRightCancelMonoid.ext_iff {M : Type u} {m₁ : AddRightCancelMonoid M} {m₂ : AddRightCancelMonoid M} :

m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd

theorem RightCancelMonoid.ext_iff {M : Type u} {m₁ : RightCancelMonoid M} {m₂ : RightCancelMonoid M} :

m₁ = m₂ ↔ HMul.hMul = HMul.hMul

theorem RightCancelMonoid.ext {M : Type u} ⦃m₁ : RightCancelMonoid M⦄ ⦃m₂ : RightCancelMonoid M⦄ (h_mul : HMul.hMul = HMul.hMul) :

m₁ = m₂

theorem AddCancelMonoid.toAddLeftCancelMonoid_injective {M : Type u} :

Function.Injective (@AddCancelMonoid.toAddLeftCancelMonoid M)

theorem CancelMonoid.toLeftCancelMonoid_injective {M : Type u} :

Function.Injective (@CancelMonoid.toLeftCancelMonoid M)

theorem AddCancelMonoid.ext {M : Type u_1} ⦃m₁ : AddCancelMonoid M⦄ ⦃m₂ : AddCancelMonoid M⦄ (h_mul : HAdd.hAdd = HAdd.hAdd) :

m₁ = m₂

theorem CancelMonoid.ext_iff {M : Type u_1} {m₁ : CancelMonoid M} {m₂ : CancelMonoid M} :

m₁ = m₂ ↔ HMul.hMul = HMul.hMul

theorem AddCancelMonoid.ext_iff {M : Type u_1} {m₁ : AddCancelMonoid M} {m₂ : AddCancelMonoid M} :

m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd

theorem CancelMonoid.ext {M : Type u_1} ⦃m₁ : CancelMonoid M⦄ ⦃m₂ : CancelMonoid M⦄ (h_mul : HMul.hMul = HMul.hMul) :

m₁ = m₂

theorem AddCancelCommMonoid.toAddCommMonoid_injective {M : Type u} :

Function.Injective (@AddCancelCommMonoid.toAddCommMonoid M)

theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} :

Function.Injective (@CancelCommMonoid.toCommMonoid M)

theorem AddCancelCommMonoid.ext {M : Type u_1} ⦃m₁ : AddCancelCommMonoid M⦄ ⦃m₂ : AddCancelCommMonoid M⦄ (h_mul : HAdd.hAdd = HAdd.hAdd) :

m₁ = m₂

theorem CancelCommMonoid.ext_iff {M : Type u_1} {m₁ : CancelCommMonoid M} {m₂ : CancelCommMonoid M} :

m₁ = m₂ ↔ HMul.hMul = HMul.hMul

theorem AddCancelCommMonoid.ext_iff {M : Type u_1} {m₁ : AddCancelCommMonoid M} {m₂ : AddCancelCommMonoid M} :

m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd

theorem CancelCommMonoid.ext {M : Type u_1} ⦃m₁ : CancelCommMonoid M⦄ ⦃m₂ : CancelCommMonoid M⦄ (h_mul : HMul.hMul = HMul.hMul) :

m₁ = m₂

theorem SubNegMonoid.ext {M : Type u_1} ⦃m₁ : SubNegMonoid M⦄ ⦃m₂ : SubNegMonoid M⦄ (h_mul : HAdd.hAdd = HAdd.hAdd) (h_inv : Neg.neg = Neg.neg) :

m₁ = m₂

theorem SubNegMonoid.ext_iff {M : Type u_1} {m₁ : SubNegMonoid M} {m₂ : SubNegMonoid M} :

m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ Neg.neg = Neg.neg

theorem DivInvMonoid.ext_iff {M : Type u_1} {m₁ : DivInvMonoid M} {m₂ : DivInvMonoid M} :

m₁ = m₂ ↔ HMul.hMul = HMul.hMul ∧ Inv.inv = Inv.inv

theorem DivInvMonoid.ext {M : Type u_1} ⦃m₁ : DivInvMonoid M⦄ ⦃m₂ : DivInvMonoid M⦄ (h_mul : HMul.hMul = HMul.hMul) (h_inv : Inv.inv = Inv.inv) :

m₁ = m₂

theorem AddGroup.toSubNegAddMonoid_injective {G : Type u_1} :

Function.Injective (@AddGroup.toSubNegMonoid G)

theorem Group.toDivInvMonoid_injective {G : Type u_1} :

Function.Injective (@Group.toDivInvMonoid G)

theorem AddGroup.ext {G : Type u_1} ⦃g₁ : AddGroup G⦄ ⦃g₂ : AddGroup G⦄ (h_mul : Add.add = Add.add) :

g₁ = g₂

theorem AddGroup.ext_iff {G : Type u_1} {g₁ : AddGroup G} {g₂ : AddGroup G} :

g₁ = g₂ ↔ Add.add = Add.add

theorem Group.ext_iff {G : Type u_1} {g₁ : Group G} {g₂ : Group G} :

g₁ = g₂ ↔ Mul.mul = Mul.mul

theorem Group.ext {G : Type u_1} ⦃g₁ : Group G⦄ ⦃g₂ : Group G⦄ (h_mul : Mul.mul = Mul.mul) :

g₁ = g₂

theorem AddCommGroup.toAddGroup_injective {G : Type u_1} :

Function.Injective (@AddCommGroup.toAddGroup G)

theorem CommGroup.toGroup_injective {G : Type u_1} :

Function.Injective (@CommGroup.toGroup G)

theorem AddCommGroup.ext {G : Type u_1} ⦃g₁ : AddCommGroup G⦄ ⦃g₂ : AddCommGroup G⦄ (h_mul : Add.add = Add.add) :

g₁ = g₂

theorem CommGroup.ext_iff {G : Type u_1} {g₁ : CommGroup G} {g₂ : CommGroup G} :

g₁ = g₂ ↔ Mul.mul = Mul.mul

theorem AddCommGroup.ext_iff {G : Type u_1} {g₁ : AddCommGroup G} {g₂ : AddCommGroup G} :

g₁ = g₂ ↔ Add.add = Add.add

theorem CommGroup.ext {G : Type u_1} ⦃g₁ : CommGroup G⦄ ⦃g₂ : CommGroup G⦄ (h_mul : Mul.mul = Mul.mul) :

g₁ = g₂