English
The nilpotency class of the product ∀ i, Gs i equals the supremum of the nilpotency classes of the factors.
Русский
Класс нильпотентности произведения по индексу равен супремуму классов нильпотентности факторов.
LaTeX
$$$\\operatorname{nilpotencyClass}(\\forall i, Gs(i)) = \\sup_i \\operatorname{nilpotencyClass}(Gs(i))$$$
Lean4
/-- The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors -/
theorem nilpotencyClass_pi [Fintype η] [∀ i, IsNilpotent (Gs i)] :
Group.nilpotencyClass (∀ i, Gs i) = Finset.univ.sup fun i => Group.nilpotencyClass (Gs i) :=
by
apply eq_of_forall_ge_iff
intro k
simp only [Finset.sup_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, lowerCentralSeries_pi_of_finite,
pi_eq_bot_iff, Finset.mem_univ, true_imp_iff]
