Structure_Induced_by_Commutative_Operation_is_Commutative
Provedcommutativitypointwise-operationsproofwiki
If the operation on T is commutative, then the pointwise operation induced on T^S is also commutative.
Preamble
import Mathlib.Algebra.Group.Pi.Basic
Formal statement
theorem Structure_Induced_by_Commutative_Operation_is_Commutative {S T : Type _} [CommSemigroup T] (f g : S → T) : f * g = g * f := by sorrySource