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