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