polyCharpoly_eq_of_basis — Mathlib

English

The polynomial polyCharpoly φ b is equal to the polynomial obtained by applying the bind₁ construction to φ with any basis b_m, after appropriate map to univariate polynomials.

Русский

Полином polyCharpoly φ b равен полиному, полученному применением константного построения bind₁ к φ с любым базисом b_m, с нужным отображением.

LaTeX

$$polyCharpoly φ b = (charpoly.univ R ιM).map (MvPolynomial.bind₁ (φ.toMvPolynomial b b_m.end))$$

Lean4

theorem polyCharpoly_eq_of_basis [DecidableEq ιM] (bₘ : Basis ιM R M) :
    polyCharpoly φ b = (charpoly.univ R ιM).map (MvPolynomial.bind₁ (φ.toMvPolynomial b bₘ.end)) := by
  rw [polyCharpoly, φ.polyCharpolyAux_basisIndep b (Module.Free.chooseBasis R M) bₘ, polyCharpolyAux]

Похожие утверждения