isNilpotent_iff — Mathlib

English

For a matrix A, IsNilpotent A is equivalent to: for all vectors v, there exists n with A^n v = 0.

Русский

Для матрицы A равносильно: для каждого вектора v существует степенная степень n такая, что A^n v = 0.

LaTeX

$$IsNilpotent(A) \\iff \\forall v, \\exists n: \\mathbb{N}, (A^n) v = 0.$$

Lean4

theorem isNilpotent_iff : IsNilpotent A ↔ ∀ v, ∃ n : ℕ, A ^ n *ᵥ v = 0 := by
  simp_rw [← isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, ← toLin'_pow, toLin'_apply]

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