Structure_Induced_by_Abelian_Group_Operation_is_Abelian_Group
Provedabelian-groupspointwise-operationsproofwiki
If G is an abelian group, then the pointwise operation induced on G^S also yields an abelian group.
Preamble
import Mathlib.Algebra.Group.Pi.Basic
Formal statement
theorem Structure_Induced_by_Abelian_Group_Operation_is_Abelian_Group {S G : Type _} [CommGroup G] (f g : S → G) : f * g = g * f := by sorrySource