English
Let F be a FunLike type with Group G, Monoid M. If x is a unit, equal at x implies equality at x⁻¹ for any two maps f,g : F.
Русский
Пусть F — класс функций; если x является единицей и f x = g x, то f x⁻¹ = g x⁻¹ для любых f,g : F.
LaTeX
$$$\\text{eq\_on\_inv}$ statement as above$$
Lean4
/-- If two homomorphisms from a division monoid to a monoid are equal at a unit `x`, then they are
equal at `x⁻¹`. -/
@[to_additive /-- If two homomorphisms from a subtraction monoid to an additive monoid are equal at an
additive unit `x`, then they are equal at `-x`. -/
]
theorem eq_on_inv {F G N} [DivisionMonoid G] [Monoid N] [FunLike F G N] [MonoidHomClass F G N] {x : G} (hx : IsUnit x)
(f g : F) (h : f x = g x) : f x⁻¹ = g x⁻¹ :=
left_inv_eq_right_inv (map_mul_eq_one f hx.inv_mul_cancel) (h.symm ▸ map_mul_eq_one g (hx.mul_inv_cancel))
