isNilpotent_finsum — Mathlib

English

General criterion: a finsum of nilpotent commuting elements is nilpotent.

Русский

Общая оценка: сумма элементов с нильпотентностью, где элементы взаимно коммутируют, нильпотентна.

LaTeX

$$$\\text{IsNilpotent} \\bigl(\\text{finsum } f\\bigr)$ при условиях, что всякое f(i) нильпотентно и все пары commuting.$$

Lean4

theorem isNilpotent_finsum {ι : Type*} {f : ι → R} (hf : ∀ b, IsNilpotent (f b)) (h_comm : ∀ i j, Commute (f i) (f j)) :
    IsNilpotent (finsum f) := by
  classical
  by_cases h : Set.Finite f.support
  · rw [finsum_def, dif_pos h]
    exact Commute.isNilpotent_sum (fun b _ ↦ hf b) (fun _ _ _ _ ↦ h_comm _ _)
  · simp only [finsum_def, dif_neg h, IsNilpotent.zero]

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