Set_of_Homomorphisms_is_Subgroup_of_All_Mappings
Provedhomomorphismsproofwikisubgroups
The set of group homomorphisms from G to an abelian group H forms a subgroup under pointwise multiplication.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Set_of_Homomorphisms_is_Subgroup_of_All_Mappings {G H : Type _} [Group G] [CommGroup H] (f g : G → H) (hf : ∀ a b : G, f (a * b) = f a * f b) (hg : ∀ a b : G, g (a * b) = g a * g b) (x : G) : (fun y => f y * g y) (x * x) = (fun y => f y * g y) x * (fun y => f y * g y) x := by sorrySource