Associativity_on_Four_Elements
Provedassociativityproofwiki
In a semigroup, the product a * b * c * d gives a unique answer regardless of how the elements are associated.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Associativity_on_Four_Elements {S : Type _} [Semigroup S] (a b c d : S) :
a * b * c * d = a * (b * (c * d)) := by sorrySource