English
Let R be a commutative ring, M a finite R-Lie module, and x,y elements of the Lie algebra L. If i and j are natural numbers with i + j = finrank_R M, then the i-th coefficient of the lieCharpoly R M x y has natDegree at most j.
Русский
Пусть R — коммутативное кольцо, M — конечная R-линейная Ли-модуль, x,y — элементы Ли-алгебры L. Если i, j ∈ ℕ и i + j = finrank_R M, то natDegree коэффициента i-го коэффициента полинома lieCharpoly_R M x y не превосходит j.
LaTeX
$$$\\forall (R) (L) (M) [\\text{CommRing } R] [\\text{LieRing } L] [\\text{LieAlgebra } R L] [\\text{Module.Finite } R L] (x,y : L) (i j : \\mathbb{N}) (hij : i + j = \\operatorname{finrank}_R M),\\quad ((\\operatorname{lieCharpoly} R M x y).coeff i).\\operatorname{natDegree} \\leq j$$$
Lean4
theorem lieCharpoly_coeff_natDegree [Nontrivial R] (i j : ℕ) (hij : i + j = finrank R M) :
((lieCharpoly R M x y).coeff i).natDegree ≤ j := by
classical
rw [← mul_one j, lieCharpoly, coeff_map]
apply MvPolynomial.aeval_natDegree_le
· apply (polyCharpoly_coeff_isHomogeneous φ (chooseBasis R L) _ _ hij).totalDegree_le
intro k
apply Polynomial.natDegree_add_le_of_degree_le
· apply (Polynomial.natDegree_C_mul_le _ _).trans
simp only [natDegree_X, le_rfl]
· simp only [natDegree_C, zero_le]
