External_Direct_Product_of_Abelian_Groups_is_Abelian_Group
Provedabeliandirect-productgroup-theoryproofwiki
If G and H are abelian groups, then their direct product G × H is abelian.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem External_Direct_Product_of_Abelian_Groups_is_Abelian_Group {G H : Type _} [CommGroup G] [CommGroup H] (a b : G × H) : a * b = b * a := by sorrySource