Elements_of_Group_with_Equal_Images_under_Homomorphisms_form_Subgroup
Provedgroup-homomorphismsproofwiki
Let G and H be groups. Let f, g : G → H be group homomorphisms. Then the set S = {x ∈ G : f(x) = g(x)} is a subgroup of G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Elements_of_Group_with_Equal_Images_under_Homomorphisms_form_Subgroup {G H : Type _} [Group G] [Group H] (f g : MonoidHom G H) (x y : G) (hx : f x = g x) (hy : f y = g y) : f (x * y) = g (x * y) := by sorrySource