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 CommMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@CommMonoid.toMonoid M)

theorem AddCommMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@AddCommMonoid.toAddMonoid 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 LeftCancelMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@LeftCancelMonoid.toMonoid M)

theorem AddLeftCancelMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@AddLeftCancelMonoid.toAddMonoid 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 RightCancelMonoid.toMonoid_injective {M : Type u} :

Function.Injective (@RightCancelMonoid.toMonoid M)

theorem AddRightCancelMonoid.toAddMonoid_injective {M : Type u} :

Function.Injective (@AddRightCancelMonoid.toAddMonoid 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 CancelMonoid.toLeftCancelMonoid_injective {M : Type u} :

Function.Injective (@CancelMonoid.toLeftCancelMonoid M)

theorem AddCancelMonoid.toAddLeftCancelMonoid_injective {M : Type u} :

Function.Injective (@AddCancelMonoid.toAddLeftCancelMonoid 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 CancelCommMonoid.toCommMonoid_injective {M : Type u} :

Function.Injective (@CancelCommMonoid.toCommMonoid M)

theorem AddCancelCommMonoid.toAddCommMonoid_injective {M : Type u} :

Function.Injective (@AddCancelCommMonoid.toAddCommMonoid 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 Group.toDivInvMonoid_injective {G : Type u_1} :

Function.Injective (@Group.toDivInvMonoid G)

theorem AddGroup.toSubNegAddMonoid_injective {G : Type u_1} :

Function.Injective (@AddGroup.toSubNegMonoid 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 CommGroup.toGroup_injective {G : Type u_1} :

Function.Injective (@CommGroup.toGroup G)

theorem AddCommGroup.toAddGroup_injective {G : Type u_1} :

Function.Injective (@AddCommGroup.toAddGroup 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₂