Associativity_of_Group_Direct_Product
Provedassociativitydirect-productgroup-theoryproofwiki
The group direct product is associative up to isomorphism: G × (H × K) ≅ (G × H) × K.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Associativity_of_Group_Direct_Product {G H K : Type _} [Group G] [Group H] [Group K] : Nonempty (G × (H × K) ≃* (G × H) × K) := by sorrySource