isNilpotent_trace_of_isNilpotent — Mathlib

English

If M is nilpotent, then its trace is nilpotent.

Русский

Если матрица M нильпотентна, то её след нильпотентен.

LaTeX

$$If $M$ is nilpotent, then $\\mathrm{trace}(M)$ is nilpotent.$$

Lean4

theorem isNilpotent_trace_of_isNilpotent (hM : IsNilpotent M) : IsNilpotent (trace M) :=
  by
  cases isEmpty_or_nonempty n
  · simp
  suffices IsNilpotent (coeff (charpolyRev M) 1) by simpa using this
  exact (isUnit_iff_coeff_isUnit_isNilpotent.mp (isUnit_charpolyRev_of_isNilpotent hM)).2 _ one_ne_zero

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