isNilpotent_charpoly_sub_pow_of_isNilpotent

English

If M is nilpotent, then M.charpoly − X^{|n|} is nilpotent.

Русский

Если матрица M нильпотентна, то charpoly(M) − X^{|n|} нильпотентен.

LaTeX

$$If $M$ is nilpotent, then $M.charpoly - X^{|n|}$ is nilpotent.$$

Lean4

theorem isNilpotent_charpoly_sub_pow_of_isNilpotent (hM : IsNilpotent M) :
    IsNilpotent (M.charpoly - X ^ (Fintype.card n)) :=
  by
  nontriviality R
  let p : R[X] := M.charpolyRev
  have hp : p - 1 = X * (p /ₘ X) := by
    conv_lhs => rw [← modByMonic_add_div p monic_X]
    simp [p, modByMonic_X]
  have : IsNilpotent (p /ₘ X) := (Polynomial.isUnit_iff'.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
  have aux : (M.charpoly - X ^ (Fintype.card n)).natDegree ≤ M.charpoly.natDegree :=
    le_trans (natDegree_sub_le _ _) (by simp)
  rw [← isNilpotent_reflect_iff aux, reflect_sub, ← reverse, M.reverse_charpoly]
  simpa [p, hp]

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