English
If η is finite and each Gs i is nilpotent, then the product ∀ i, Gs i is nilpotent.
Русский
Если η конечно и каждый Gs_i нильпотентен, тогда произведение по индексу Гс_i нильпотентно.
LaTeX
$$$\\operatorname{IsNilpotent}(\\forall i, Gs(i))$$$
Lean4
/-- n-ary products of nilpotent groups are nilpotent -/
instance isNilpotent_pi [Finite η] [∀ i, IsNilpotent (Gs i)] : IsNilpotent (∀ i, Gs i) :=
by
cases nonempty_fintype η
rw [nilpotent_iff_lowerCentralSeries]
refine ⟨Finset.univ.sup fun i => Group.nilpotencyClass (Gs i), ?_⟩
rw [lowerCentralSeries_pi_of_finite, pi_eq_bot_iff]
intro i
rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]
exact Finset.le_sup (f := fun i => Group.nilpotencyClass (Gs i)) (Finset.mem_univ i)
