Direct_Product_of_Central_Subgroup_with_Inverse_Isomorphism_is_Central_Subgroup
Provedcenterdirect-productsgroup-theoryproofwikisubgroups
Let and be groups. Let denote the center of . Let and be central subgroups of and respectively. Let where denotes isomorphism. Let such a group isomorphism be . Let be the set defined as X = \set {\tuple {x, \map \theta x^{-1} }: x \in Z} Then is a central subgroup of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Direct_Product_of_Central_Subgroup_with_Inverse_Isomorphism_is_Central_Subgroup {G H : Type _} [Group G] [Group H] (Z : Subgroup G) (W : Subgroup H) (hZ : Z ≤ Subgroup.center G) (hW : W ≤ Subgroup.center H) : Z.prod W ≤ Subgroup.center (G × H) := by sorrySource