rank_eq_natTrailingDegree — Mathlib

English

Under finiteness and basis assumptions, the rank equals the natTrailingDegree of the characteristic polynomial of the endomorphism associated to φ.

Русский

При конечности и заданном базисе ранг равен natTrailingDegree характеристического многочлена соответствующего эндоморфизма.

LaTeX

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

Lean4

theorem rank_eq_natTrailingDegree [Nontrivial R] [DecidableEq ι] : rank R L M = (polyCharpoly φ b).natTrailingDegree :=
  by apply nilRank_eq_polyCharpoly_natTrailingDegree

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