General_Associativity_Theorem
Provedassociativitygeneral-associativity-theoremnamed-theoremsproofwiki
If an operation is associative on entities, then it is associative on any number of them.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem General_Associativity_Theorem {S : Type _} [Semigroup S] (a b c : S) : a * b * c = a * (b * c) := by sorrySource