External_Direct_Product_of_Semigroups
Proveddirect-productsproofwikisemigroups
The external direct product of two semigroups is itself a semigroup.
Preamble
import Mathlib.Algebra.Group.Prod
Formal statement
theorem External_Direct_Product_of_Semigroups {S T : Type _} [Semigroup S] [Semigroup T] (a b c : S × T) : a * b * c = a * (b * c) := by sorrySource