English
The nilpotency class of a direct product equals the maximum of the nilpotency classes of its factors.
Русский
Класс нильпотентности прямого произведения равен максимуму классов его факторов.
LaTeX
$$$\\operatorname{nilpotencyClass}(G_1 \\times G_2) = \\max\\bigl(\\operatorname{nilpotencyClass}(G_1), \\operatorname{nilpotencyClass}(G_2)\\bigr)$$$
Lean4
/-- The nilpotency class of a product is the max of the nilpotency classes of the factors -/
theorem nilpotencyClass_prod [IsNilpotent G₁] [IsNilpotent G₂] :
Group.nilpotencyClass (G₁ × G₂) = max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂) :=
by
refine eq_of_forall_ge_iff fun k => ?_
simp only [max_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, lowerCentralSeries_prod, prod_eq_bot_iff]
