Epimorphism_Preserves_Inverses
Provedepimorphismsinverse-elementsproofwiki
A group homomorphism preserves inverses: f(x⁻¹) = f(x)⁻¹.
Preamble
import Mathlib.Algebra.Group.Hom.Defs
Formal statement
theorem Epimorphism_Preserves_Inverses {G H : Type _} [Group G] [Group H] (f : MonoidHom G H) (x : G) : f x⁻¹ = (f x)⁻¹ := by sorrySource