English
If all factors Gs i are nilpotent and their nilpotency classes are bounded by n, then the product ∀ i, Gs i is nilpotent.
Русский
Если все множители Gs_i нильпотентны и их классы нильпотентности ограничены верхом n, то ∀ i, Gs_i нильпотентна.
LaTeX
$$[IsNilpotent (Gs i)] for all i and nilpotencyClass(Gs i) ≤ n imply IsNilpotent(∀ i, Gs i)$$
Lean4
/-- products of nilpotent groups are nilpotent if their nilpotency class is bounded -/
theorem isNilpotent_pi_of_bounded_class [∀ i, IsNilpotent (Gs i)] (n : ℕ) (h : ∀ i, Group.nilpotencyClass (Gs i) ≤ n) :
IsNilpotent (∀ i, Gs i) := by
rw [nilpotent_iff_lowerCentralSeries]
refine ⟨n, ?_⟩
rw [eq_bot_iff]
apply le_trans (lowerCentralSeries_pi_le _)
rw [← eq_bot_iff, pi_eq_bot_iff]
intro i
apply lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (h i)
