mathlib3 documentation

algebra.group.ext

Extensionality lemmas for monoid and group structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[ext]
theorem monoid.ext {M : Type u} ⦃m₁ m₂ : monoid M⦄ (h_mul : monoid.mul = monoid.mul) :
m₁ = m₂
source
@[ext]
theorem add_monoid.ext {M : Type u} ⦃m₁ m₂ : add_monoid M⦄ (h_mul : add_monoid.add = add_monoid.add) :
m₁ = m₂
source
theorem comm_monoid.to_monoid_injective {M : Type u} :
function.injective (comm_monoid.to_monoid M)
source
theorem add_comm_monoid.to_add_monoid_injective {M : Type u} :
function.injective (add_comm_monoid.to_add_monoid M)
source
@[ext]
theorem comm_monoid.ext {M : Type u_1} ⦃m₁ m₂ : comm_monoid M⦄ (h_mul : comm_monoid.mul = comm_monoid.mul) :
m₁ = m₂
source
@[ext]
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₂
source
theorem left_cancel_monoid.to_monoid_injective {M : Type u} :
function.injective (left_cancel_monoid.to_monoid M)
source
theorem add_left_cancel_monoid.to_add_monoid_injective {M : Type u} :
function.injective (add_left_cancel_monoid.to_add_monoid M)
source
@[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₂
source
@[ext]
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₂
source
theorem add_right_cancel_monoid.to_add_monoid_injective {M : Type u} :
function.injective (add_right_cancel_monoid.to_add_monoid M)
source
theorem right_cancel_monoid.to_monoid_injective {M : Type u} :
function.injective (right_cancel_monoid.to_monoid M)
source
@[ext]
theorem add_right_cancel_monoid.ext {M : Type u} ⦃m₁ m₂ : add_right_cancel_monoid M⦄ (h_mul : add_right_cancel_monoid.add = add_right_cancel_monoid.add) :
m₁ = m₂
source
@[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₂
source
theorem add_cancel_monoid.to_left_cancel_add_monoid_injective {M : Type u} :
function.injective (add_cancel_monoid.to_add_left_cancel_monoid M)
source
theorem cancel_monoid.to_left_cancel_monoid_injective {M : Type u} :
function.injective (cancel_monoid.to_left_cancel_monoid M)
source
@[ext]
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₂
source
@[ext]
theorem cancel_monoid.ext {M : Type u_1} ⦃m₁ m₂ : cancel_monoid M⦄ (h_mul : cancel_monoid.mul = cancel_monoid.mul) :
m₁ = m₂
source
theorem add_cancel_comm_monoid.to_add_comm_monoid_injective {M : Type u} :
function.injective (add_cancel_comm_monoid.to_add_comm_monoid M)
source
theorem cancel_comm_monoid.to_comm_monoid_injective {M : Type u} :
function.injective (cancel_comm_monoid.to_comm_monoid M)
source
@[ext]
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₂
source
@[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₂
source
@[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₂
source
@[ext]
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₂
source
@[ext]
theorem group.ext {G : Type u_1} ⦃g₁ g₂ : group G⦄ (h_mul : group.mul = group.mul) :
g₁ = g₂
source
@[ext]
theorem add_group.ext {G : Type u_1} ⦃g₁ g₂ : add_group G⦄ (h_mul : add_group.add = add_group.add) :
g₁ = g₂
source
@[ext]
theorem comm_group.ext {G : Type u_1} ⦃g₁ g₂ : comm_group G⦄ (h_mul : comm_group.mul = comm_group.mul) :
g₁ = g₂
source
@[ext]
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₂