External_Direct_Product_Associativity
Proveddirect-productsexternal-direct-productsproofwiki
If the operations on S and T are associative, then the componentwise operation on S × T is also associative.
Preamble
import Mathlib.Algebra.Group.Prod
Formal statement
theorem External_Direct_Product_Associativity {S T : Type _} [Semigroup S] [Semigroup T] (a b c : S × T) : a * b * c = a * (b * c) := by sorrySource