English
For a nontrivial base ring R, the natDegree of lieCharpoly equals the finite rank finrank_R M of the module M.
Русский
При ненулевом кольце R натуральная степень натуральной характеристики lieCharpoly равна конечной размерности finrank_R M модуля M.
LaTeX
$$$\\operatorname{natDegree}(\\operatorname{lieCharpoly}_R M x y) = \\operatorname{finrank}_R M$$$
Lean4
theorem lieCharpoly_map_eval (r : R) : (lieCharpoly R M x y).map (evalRingHom r) = (φ (r • y + x)).charpoly :=
by
rw [lieCharpoly, map_map]
set b := chooseBasis R L
have aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = b.repr (r • y + x) := by ext i; simp [mul_comm r]
simp_rw [← coe_aeval_eq_evalRingHom, ← AlgHom.comp_toRingHom, MvPolynomial.comp_aeval, map_add, map_mul, aeval_C,
Algebra.algebraMap_self, RingHom.id_apply, aeval_X, aux, MvPolynomial.coe_aeval_eq_eval,
polyCharpoly_map_eq_charpoly, LieHom.coe_toLinearMap]
