English
A finite sum of pairwise commuting nilpotent elements is nilpotent.
Русский
Конечная сумма взаимно коммутирующих нильпотентных элементов нильпотентна.
LaTeX
$$$\\forall i, f(i)\\text{ nilpotent} \\Rightarrow \\text{IsNilpotent}(\\text{finsum } f)$$$
Lean4
protected theorem isNilpotent_sum {ι : Type*} {s : Finset ι} {f : ι → R} (hnp : ∀ i ∈ s, IsNilpotent (f i))
(h_comm : ∀ i j, i ∈ s → j ∈ s → Commute (f i) (f j)) : IsNilpotent (∑ i ∈ s, f i) := by
classical
induction s using Finset.induction with
| empty => simp
| insert j s hj ih => ?_
rw [Finset.sum_insert hj]
apply Commute.isNilpotent_add
· exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))
· apply hnp; simp
· exact ih (fun i hi ↦ hnp i (by simp [hi])) (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))
