Theorems · Theorem · group theory

IsUnit.eq_on_inv

∀ {F : Type u_1} {G : Type u_2} {N : Type u_3} [inst : DivisionMonoid G] [inst_1 : Monoid N] [inst_2 : FunLike F G N]
  [MonoidHomClass F G N] {x : G}, IsUnit x → ∀ (f g : F), f x = g x → f x⁻¹ = g x⁻¹

If two homomorphisms from a division monoid to a monoid are equal at a unit x, then they are equal at x⁻¹.

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

2 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

DivisionMonoidMonoidFunLikeMonoidHomClass