mathlib documentation

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 monoid_hom.map_div, monoid_hom.map_pow etc.

Tags #

monoid, group, extensionality

@[ext]
theorem monoid.ext {M : Type u} ⦃m₁ m₂ : monoid M⦄ (h_mul : monoid.mul = monoid.mul) :
m₁ = m₂
theorem add_monoid.ext {M : Type u} ⦃m₁ m₂ : add_monoid M⦄ (h_mul : add_monoid.add = add_monoid.add) :
m₁ = m₂
@[ext]
theorem comm_monoid.ext {M : Type u_1} ⦃m₁ m₂ : comm_monoid M⦄ (h_mul : comm_monoid.mul = comm_monoid.mul) :
m₁ = m₂
theorem add_comm_monoid.ext {M : Type u_1} ⦃m₁ m₂ : add_comm_monoid M⦄ (h_mul : add_comm_monoid.add = add_comm_monoid.add) :
m₁ = m₂
@[ext]
theorem left_cancel_monoid.ext {M : Type u} ⦃m₁ m₂ : left_cancel_monoid M⦄ (h_mul : left_cancel_monoid.mul = left_cancel_monoid.mul) :
m₁ = m₂
theorem add_left_cancel_monoid.ext {M : Type u} ⦃m₁ m₂ : add_left_cancel_monoid M⦄ (h_mul : add_left_cancel_monoid.add = add_left_cancel_monoid.add) :
m₁ = m₂
@[ext]
theorem right_cancel_monoid.ext {M : Type u} ⦃m₁ m₂ : right_cancel_monoid M⦄ (h_mul : right_cancel_monoid.mul = right_cancel_monoid.mul) :
m₁ = m₂
theorem add_cancel_monoid.ext {M : Type u_1} ⦃m₁ m₂ : add_cancel_monoid M⦄ (h_mul : add_cancel_monoid.add = add_cancel_monoid.add) :
m₁ = m₂
@[ext]
theorem cancel_monoid.ext {M : Type u_1} ⦃m₁ m₂ : cancel_monoid M⦄ (h_mul : cancel_monoid.mul = cancel_monoid.mul) :
m₁ = m₂
theorem add_cancel_comm_monoid.ext {M : Type u_1} ⦃m₁ m₂ : add_cancel_comm_monoid M⦄ (h_mul : add_cancel_comm_monoid.add = add_cancel_comm_monoid.add) :
m₁ = m₂
@[ext]
theorem cancel_comm_monoid.ext {M : Type u_1} ⦃m₁ m₂ : cancel_comm_monoid M⦄ (h_mul : cancel_comm_monoid.mul = cancel_comm_monoid.mul) :
m₁ = m₂
@[ext]
theorem div_inv_monoid.ext {M : Type u_1} ⦃m₁ m₂ : div_inv_monoid M⦄ (h_mul : div_inv_monoid.mul = div_inv_monoid.mul) (h_inv : div_inv_monoid.inv = div_inv_monoid.inv) :
m₁ = m₂
theorem sub_neg_monoid.ext {M : Type u_1} ⦃m₁ m₂ : sub_neg_monoid M⦄ (h_mul : sub_neg_monoid.add = sub_neg_monoid.add) (h_inv : sub_neg_monoid.neg = sub_neg_monoid.neg) :
m₁ = m₂
@[ext]
theorem group.ext {G : Type u_1} ⦃g₁ g₂ : group G⦄ (h_mul : group.mul = group.mul) :
g₁ = g₂
theorem add_group.ext {G : Type u_1} ⦃g₁ g₂ : add_group G⦄ (h_mul : add_group.add = add_group.add) :
g₁ = g₂
@[ext]
theorem comm_group.ext {G : Type u_1} ⦃g₁ g₂ : comm_group G⦄ (h_mul : comm_group.mul = comm_group.mul) :
g₁ = g₂
theorem add_comm_group.ext {G : Type u_1} ⦃g₁ g₂ : add_comm_group G⦄ (h_mul : add_comm_group.add = add_comm_group.add) :
g₁ = g₂