polyCharpoly_coeff_rank_ne_zero — Mathlib

English

The rank of M as a Lie module equals the natTrailingDegree of the polyCharpoly of φ with respect to basis b.

Русский

Ранг M как Ли-модуля равен natTrailingDegree полиномa polyCharpoly φ b по базису b.

LaTeX

$$rank R L M = (polyCharpoly φ b).natTrailingDegree$$

Lean4

theorem polyCharpoly_coeff_rank_ne_zero [Nontrivial R] [DecidableEq ι] : (polyCharpoly φ b).coeff (rank R L M) ≠ 0 :=
  polyCharpoly_coeff_nilRank_ne_zero _ _

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