aeval_toMvPolynomial — Mathlib

English

The equality between two constructions involving finSuccEquiv and rename when applied to a polynomial φ holds as described by the given composition.

Русский

Сохранено равенство между двумя конструкциями, включающими finSuccEquiv и rename, при применении к полиному φ, как указано в составе.

LaTeX

$$$((\mathrm{finSuccEquiv}\,R\,n) (\mathrm{rename}((\mathrm{Equiv.optionCongr}\ e).trans(\mathrm{finSuccEquiv}\ n).symm)\ \phi)) = \mathrm{Polynomial.map}(\mathrm{rename}(e).toRingHom) (\mathrm{optionEquivLeft}\;R\sigma\phi)$$$

Lean4

@[simp]
theorem aeval_toMvPolynomial (f : σ → S) (i : σ) (p : R[X]) : aeval f (p.toMvPolynomial i) = Polynomial.aeval (f i) p :=
  DFunLike.congr_fun (aeval_comp_toMvPolynomial ..) p

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