English
There exists a universal characteristic polynomial for n × n matrices over R, obtained as the characteristic polynomial of mvPolynomialX n n R with entries X_{ij}. Its i-th coefficient is homogeneous of degree n − i.
Русский
Существует универсальный характеристический полином для матриц размером n × n над кольцом R, получаемый как характеристический полином mvPolynomialX n n R со значениями X_{ij}. i-й коэффициент гомогенный степенью n − i.
LaTeX
$$$\\text{univ} : \\text{Polynomial} (\\mathrm{MvPolynomial} (n \\times n) R) = \\mathrm{charpoly}(\\mathrm{mvPolynomialX} n n R)$$$
Lean4
/-- The universal characteristic polynomial for `n × n`-matrices,
is the characteristic polynomial of `Matrix.mvPolynomialX n n ℤ` with entries `Xᵢⱼ`.
Its `i`-th coefficient is a homogeneous polynomial of degree `n - i`,
see `Matrix.charpoly.univ_coeff_isHomogeneous`.
By evaluating the coefficients at the entries of a matrix `M`,
one obtains the characteristic polynomial of `M`,
see `Matrix.charpoly.univ_map_eval₂Hom`. -/
noncomputable abbrev univ : Polynomial (MvPolynomial (n × n) R) :=
charpoly <| mvPolynomialX n n R
