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