English
polyCharpolyAux is the polynomial-valued object that, given φ, b, b_m, yields a polynomial encoding the family of characteristic polynomials of φ x acting on M.
Русский
polyCharpolyAux — это полином, зависящий от φ, b, b_m, который кодирует семейство характеристических полиномов φ x, действующего на M.
LaTeX
$$polyCharpolyAux : Polynomial (MvPolynomial ι R)$$
Lean4
/-- (Implementation detail, see `LinearMap.polyCharpoly`.)
Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear map.
Let `b` be a basis of `L` and `bₘ` a basis of `M`.
Then `LinearMap.polyCharpolyAux φ b bₘ` is the polynomial that evaluates on elements `x` of `L`
to the characteristic polynomial of `φ x` acting on `M`.
This definition does not depend on the choice of `bₘ`
(see `LinearMap.polyCharpolyAux_basisIndep`). -/
noncomputable def polyCharpolyAux : Polynomial (MvPolynomial ι R) :=
(charpoly.univ R ιM).map <| MvPolynomial.bind₁ (φ.toMvPolynomial b bₘ.end)
