isNilpotent_toLin'_iff — Mathlib

English

For a finite matrix A, IsNilpotent A.toLin' iff IsNilpotent A.

Русский

Для матрицы A верно: IsNilpotent A.toLin' ⇔ IsNilpotent A.

LaTeX

$$IsNilpotent A.toLin' ↔ IsNilpotent A$$

Lean4

@[simp]
theorem isNilpotent_toLin'_iff {ι : Type*} [DecidableEq ι] [Fintype ι] [CommSemiring R] (A : Matrix ι ι R) :
    IsNilpotent A.toLin' ↔ IsNilpotent A :=
  by
  have : A.toLin'.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) = A := LinearMap.toMatrix'_toLin' A
  conv_rhs => rw [← this]
  rw [LinearMap.isNilpotent_toMatrix_iff]

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