lieCharpoly_natDegree — Mathlib

English

For a fixed r ∈ R, the polynomial LieCharpoly maps under evaluation at r to the charpoly of the operator φ(r y + x).

Русский

Для фиксированного r ∈ R полином LieCharpoly отображается под операцией оценки в φ( r y + x ).

LaTeX

$$$\\operatorname{map}(\\operatorname{evalRingHom} r)(\\operatorname{lieCharpoly}_R M x y) = \\operatorname{charpoly}(\\varphi(r\\,y + x))$$$

Lean4

theorem lieCharpoly_natDegree [Nontrivial R] : (lieCharpoly R M x y).natDegree = finrank R M := by
  rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]

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