English
Let φ be a family of endomorphisms on a finite free module M over a commutative ring R, measured with respect to a basis b of L. Then for all natural numbers i and j with i + j equal to the dimension finrank_R M, the i-th coefficient of the characteristic polynomial polyCharpoly φ b is a homogeneous polynomial of total degree j.
Русский
Пусть φ задаёт семейство линейных отображений на конечном свободном модуле M над кольцом R, измеряемое по базису b модуля L. Тогда для всех i, j ∈ ℕ такие, что i + j = finrank_R M, i-й коэффициент полиномa характеристик polyCharpoly φ b является однородной полиномом степени j.
LaTeX
$$$\forall i,j \in \mathbb{N},\ i+j=\operatorname{finrank}_R M \Rightarrow ((\mathrm{polyCharpoly}\,\phi\, b).\mathrm{coeff}\ i) \text{ is homogeneous of degree } j$$$
Lean4
theorem polyCharpoly_coeff_isHomogeneous (i j : ℕ) (hij : i + j = finrank R M) [Nontrivial R] :
((polyCharpoly φ b).coeff i).IsHomogeneous j :=
by
rw [finrank_eq_card_chooseBasisIndex] at hij
rw [polyCharpoly, polyCharpolyAux, Polynomial.coeff_map, ← one_mul j]
apply (charpoly.univ_coeff_isHomogeneous _ _ _ _ hij).eval₂
· exact fun r ↦ MvPolynomial.isHomogeneous_C _ _
· exact LinearMap.toMvPolynomial_isHomogeneous _ _ _
