English
Variant of the previous inv-equality lemma for a general MonoidHom context.
Русский
Вариант предыдущего леммы о равенстве на инверсии в общем контексте монадного гомоморфизма.
LaTeX
$$$f(x) = g(x) \\Rightarrow f(x^{-1}) = g(x^{-1})$$$
Lean4
/-- If two homomorphism from a group to a monoid are equal at `x`, then they are equal at `x⁻¹`. -/
@[to_additive /-- If two homomorphism from an additive group to an additive monoid are equal at `x`,
then they are equal at `-x`. -/
]
theorem eq_on_inv {F G M} [Group G] [Monoid M] [FunLike F G M] [MonoidHomClass F G M] (f g : F) {x : G}
(h : f x = g x) : f x⁻¹ = g x⁻¹ :=
(Group.isUnit x).eq_on_inv f g h
