Commutativity_of_Group_Direct_Product
Provedcommutativitydirect-productgroup-theoryproofwiki
The group direct product G × H is isomorphic to H × G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Commutativity_of_Group_Direct_Product {G H : Type _} [Group G] [Group H] : Nonempty (G × H ≃* H × G) := by sorrySource