Group_Homomorphism_of_Product_with_Inverse
Provedgroup-homomorphismsproofwiki
For a group homomorphism f, f(x * y⁻¹) = f(x) * f(y)⁻¹.
Preamble
import Mathlib.Algebra.Group.Hom.Defs
Formal statement
theorem Group_Homomorphism_of_Product_with_Inverse {G H : Type _} [Group G] [Group H] (f : MonoidHom G H) (x y : G) : f (x * y⁻¹) = f x * (f y)⁻¹ := by sorrySource