isNilpotent_toMatrix_iff — Mathlib

English

For a finite-dimensional space with basis b, IsNilpotent f iff IsNilpotent (toMatrix b b f).

Русский

Для конечномерного пространства с базисом b нильпоследовательность линейного оператора равна нильпотентности матрицы представления.

LaTeX

$$IsNilpotent (toMatrix b b f) ↔ IsNilpotent f$$

Lean4

@[simp]
theorem isNilpotent_toMatrix_iff (b : Basis ι R M) (f : M →ₗ[R] M) : IsNilpotent (toMatrix b b f) ↔ IsNilpotent f :=
  by
  refine exists_congr fun k ↦ ?_
  rw [toMatrix_pow]
  exact (toMatrix b b).map_eq_zero_iff

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