univ_natDegree — Mathlib

English

The natDegree of the universal characteristic polynomial equals the cardinality of n; equivalently natDegree(charpoly.univ R n) = Fintype.card n.

Русский

natDegree(универсального характеристического полинома) равен мощности множества n; эквивалентно natDegree(charpoly.univ R n) = Fintype.card n.

LaTeX

$$$\\operatorname{natDegree}(\\mathrm{charpoly.univ}\\,R\,n) = \\operatorname{Fintype.card} n$$$

Lean4

theorem univ_natDegree [Nontrivial R] : (univ R n).natDegree = Fintype.card n :=
  charpoly_natDegree_eq_dim (mvPolynomialX n n R)

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