Internal_and_External_Group_Direct_Products_are_Isomorphic

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

direct-productsgroup-theoryisomorphismsproofwiki

Let $G$ be a group whose identity is $e$ . Then $G$ is the (external) group direct product of $G_1, G_2, \ldots, G_n$ $G$ is the internal group direct product of $N_1, N_2, \ldots, N_n$ such that $\forall i \in \N_n: N_i \cong G_i$ where $\cong$ denotes (group) isomorphism $\N_n$ denotes $\set {1, 2, \ldots, n}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Internal_and_External_Group_Direct_Products_are_Isomorphic {G : Type _} [Group G] (H K : Subgroup G) (hHK : H ⊓ K = ⊥) (hGen : H ⊔ K = ⊤) (hComm : ∀ (h : G), h ∈ H → ∀ (k : G), k ∈ K → h * k = k * h) : Nonempty (G ≃* (H × K)) := by sorry

Source

https://proofwiki.org/wiki/Internal_and_External_Group_Direct_Products_are_Isomorphic

View graph