isNilpotent_iff_forall_row — Mathlib

English

IsNilpotent A is equivalent to: for every row index i, there exists n with the i-th row of A^n equal to the zero row.

Русский

IsNilpotent A эквивалентно: для каждого индекса строки i существует n, при котором i-я строка A^n равна нулевой строке.

LaTeX

$$IsNilpotent A \\iff \\forall i, \\exists n: (A^n).row_i = 0.$$

Lean4

theorem isNilpotent_iff_forall_row : IsNilpotent A ↔ ∀ i, ∃ n : ℕ, (A ^ n).row i = 0 :=
  by
  rw [← isNilpotent_transpose_iff, isNilpotent_iff]
  refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩
  · obtain ⟨n, hn⟩ := h (Pi.single i 1)
    exact ⟨n, by simpa [← transpose_pow] using hn⟩
  · choose n hn using h
    suffices ∀ i, (A ^ ⨆ j, n j) i = 0 from ⟨⨆ j, n j, by simp [mulVec_eq_sum, this]⟩
    exact fun i ↦ pow_row_eq_zero_of_le (hn i) (Finite.le_ciSup n i)

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