isNilpotent_sum — Mathlib

English

If R is a commutative semiring and each f(i) is nilpotent for i in a finite index set s, then the finite sum over s of f(i) is nilpotent.

Русский

Пусть R — коммутативная полугруппа (полуг ring) с единицей, и для каждого i в конечном индексе s элемент f(i) нилпотентен; тогда сумма ∑_{i∈s} f(i) нилпотентна.

LaTeX

$$$ \\forall i\\in s,\\ IsNilpotent(f(i)) \\Rightarrow \\IsNilpotent\\left(\\sum_{i\\in s} f(i)\\right)$$$

Lean4

theorem isNilpotent_sum {ι : Type*} {s : Finset ι} {f : ι → R} (hnp : ∀ i ∈ s, IsNilpotent (f i)) :
    IsNilpotent (∑ i ∈ s, f i) :=
  Commute.isNilpotent_sum hnp fun _ _ _ _ ↦ Commute.all _ _

Похожие утверждения