isUnit_charpolyRev_of_isNilpotent

English

If M is nilpotent, then the reverse characteristic polynomial M.charpolyRev is a unit in the polynomial ring over R.

Русский

Если матрица M нильпотентна, то обратный характеристический многочлен M.charpolyRev является единицей в кольце многочленов над R.

LaTeX

$$If $M$ is nilpotent, then $M.charpolyRev$ is a unit in $R[X]$.$$

Lean4

theorem isUnit_charpolyRev_of_isNilpotent (hM : IsNilpotent M) : IsUnit M.charpolyRev :=
  by
  obtain ⟨k, hk⟩ := hM
  replace hk : 1 - (X : R[X]) • M.map C ∣ 1 :=
    by
    convert one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k
    rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]
  apply isUnit_of_dvd_one
  rw [← det_one (R := R[X]) (n := n)]
  exact map_dvd detMonoidHom hk

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