English
The direct product of two nilpotent groups is nilpotent.
Русский
Прямое произведение двух нильпотентных групп нильпотентно.
LaTeX
$$$\\text{IsNilpotent}(G_1) \\wedge \\text{IsNilpotent}(G_2) \\Rightarrow \\text{IsNilpotent}(G_1 \\times G_2)$$$
Lean4
/-- Products of nilpotent groups are nilpotent -/
instance isNilpotent_prod [IsNilpotent G₁] [IsNilpotent G₂] : IsNilpotent (G₁ × G₂) :=
by
rw [nilpotent_iff_lowerCentralSeries]
refine ⟨max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂), ?_⟩
rw [lowerCentralSeries_prod, lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]
