polyCharpolyAux_map_eval — Mathlib

English

Congruence simplifications provide basis-independent equalities for polyCharpolyAux under equivalences of bases.

Русский

Схемы сведения по конгруэнтности дают базисно-независимые равенства polyCharpolyAux при эквивалентностях базисов.

LaTeX

$$polyCharpolyAux φ b b_m = polyCharpolyAux φ b b_m_1 → ...$$

Lean4

theorem polyCharpolyAux_map_eval [Module.Finite R M] [Module.Free R M] (x : ι → R) :
    (polyCharpolyAux φ b bₘ).map (MvPolynomial.eval x) = (φ (b.repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly :=
  by
  simp only [← polyCharpolyAux_map_eq_charpoly φ b bₘ, LinearEquiv.apply_symm_apply, Finsupp.equivFunOnFinite,
    Equiv.coe_fn_symm_mk, Finsupp.coe_mk]

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