# 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

m₁ = m₂
theorem Monoid.ext {M : Type u} ⦃m₁ : ⦃m₂ : (h_mul : HMul.hMul = HMul.hMul) :
m₁ = m₂
m₁ = m₂
theorem CommMonoid.ext {M : Type u_1} ⦃m₁ : ⦃m₂ : (h_mul : HMul.hMul = HMul.hMul) :
m₁ = m₂
m₁ = m₂
theorem LeftCancelMonoid.ext {M : Type u} ⦃m₁ : ⦃m₂ : (h_mul : HMul.hMul = HMul.hMul) :
m₁ = m₂
m₁ = m₂
theorem RightCancelMonoid.ext {M : Type u} ⦃m₁ : ⦃m₂ : (h_mul : HMul.hMul = HMul.hMul) :
m₁ = m₂
m₁ = m₂
theorem CancelMonoid.ext {M : Type u_1} ⦃m₁ : ⦃m₂ : (h_mul : HMul.hMul = HMul.hMul) :
m₁ = m₂
m₁ = m₂
theorem CancelCommMonoid.ext {M : Type u_1} ⦃m₁ : ⦃m₂ : (h_mul : HMul.hMul = HMul.hMul) :
m₁ = m₂