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 Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄ (h_mul : HMul.hMul = HMul.hMul) :

m₁ = m₂

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

m₁ = m₂

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

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

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

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

theorem CommMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@toMonoid M)

theorem AddCommMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@toAddMonoid M)

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

m₁ = m₂

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

m₁ = m₂

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

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

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

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

theorem LeftCancelMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@toMonoid M)

theorem AddLeftCancelMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@toAddMonoid M)

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

m₁ = m₂

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

m₁ = m₂

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

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

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

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

theorem RightCancelMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@toMonoid M)

theorem AddRightCancelMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@toAddMonoid M)

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

m₁ = m₂

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

m₁ = m₂

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

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

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

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

theorem CancelMonoid.toLeftCancelMonoid_injective {M : Type u} :

Function.Injective (@toLeftCancelMonoid M)

theorem AddCancelMonoid.toAddLeftCancelMonoid_injective {M : Type u} :

Function.Injective (@toAddLeftCancelMonoid M)

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

m₁ = m₂

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

m₁ = m₂

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

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

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

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

theorem CancelMonoid.toRightCancelMonoid_injective {M : Type u} :

Function.Injective (@toRightCancelMonoid M)

theorem AddCancelMonoid.toAddRightCancelMonoid_injective {M : Type u} :

Function.Injective (@toAddRightCancelMonoid M)

theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} :

Function.Injective (@toCommMonoid M)

theorem AddCancelCommMonoid.toAddCommMonoid_injective {M : Type u} :

Function.Injective (@toAddCommMonoid M)

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

m₁ = m₂

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

m₁ = m₂

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

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

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

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

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

m₁ = m₂

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

m₁ = m₂

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

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

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

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

theorem Group.toDivInvMonoid_injective {G : Type u_1} :

Function.Injective (@toDivInvMonoid G)

theorem AddGroup.toSubNegAddMonoid_injective {G : Type u_1} :

Function.Injective (@toSubNegMonoid G)

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

g₁ = g₂

theorem AddGroup.ext {G : Type u_1} ⦃g₁ g₂ : AddGroup G⦄ (h_add : HAdd.hAdd = HAdd.hAdd) :

g₁ = g₂

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

g₁ = g₂ ↔ HAdd.hAdd = HAdd.hAdd

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

g₁ = g₂ ↔ HMul.hMul = HMul.hMul

theorem CommGroup.toGroup_injective {G : Type u_1} :

Function.Injective (@toGroup G)

theorem AddCommGroup.toAddGroup_injective {G : Type u_1} :

Function.Injective (@toAddGroup G)

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

g₁ = g₂

theorem AddCommGroup.ext {G : Type u_1} ⦃g₁ g₂ : AddCommGroup G⦄ (h_add : HAdd.hAdd = HAdd.hAdd) :

g₁ = g₂

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

g₁ = g₂ ↔ HAdd.hAdd = HAdd.hAdd

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

g₁ = g₂ ↔ HMul.hMul = HMul.hMul