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 {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 {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 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 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 {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 {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 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 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 {G : Type u_1} ⦃g₁ : CommGroup G⦄ ⦃g₂ : CommGroup G⦄ (h_mul : Mul.mul = Mul.mul) :

g₁ = g₂