English
Group homomorphisms preserve inverse. Let G be a group and H a division monoid; for any f: G →* H and a ∈ G, f(a⁻¹) = f(a)⁻¹.
Русский
Гомоморфизмы групп сохраняют обратное. Пусть G — группа, H — дивизионный моноид; для любого f: G →* H и любого a ∈ G выполняется f(a⁻¹) = f(a)⁻¹.
LaTeX
$$$$ \forall a \in G,\ f(a^{-1}) = f(a)^{-1}. $$$$
Lean4
/-- Group homomorphisms preserve inverse.
See note [hom simp lemma priority] -/
@[to_additive (attr := simp mid) /-- Additive group homomorphisms preserve negation. -/
]
theorem map_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a : G) : f a⁻¹ = (f a)⁻¹ :=
eq_inv_of_mul_eq_one_left <| map_mul_eq_one f <| inv_mul_cancel _
