isNilpotent_iff_forall_col — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isNilpotent_iff_forall_col : IsNilpotent A ↔ ∀ i, ∃ n : ℕ, (A ^ n).col i = 0 :=
  by
  rw [← isNilpotent_transpose_iff, isNilpotent_iff_forall_row]
  simp_rw [← transpose_pow, row_transpose]

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