eval₂_const_pUnitAlgEquiv_symm — Mathlib

English

For any mv-polynomial f in PUnit, and φ, a, the evaluation under the symmetric map corresponds to evaluating f in the univariate polynomial ring via the isomorphism.

Русский

Для mv-многочлена f в PUnit и отображений φ, a вычисление через симметричное отображение соответствует вычислению f в однопеременном кольце полиномов через изоморфизм.

LaTeX

$$$$ \\text{eval₂}_\\text{pUnitAlgEquiv}^{-1}(f) = \\text{eval₂}_\\text{Polynomial}(f). $$$$

Lean4

theorem eval₂_const_pUnitAlgEquiv_symm {f : Polynomial R} {φ : R →+* S} {a : S} :
    ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ (fun _ ↦ a) = f.eval₂ φ a := by
  rw [eval₂_pUnitAlgEquiv_symm]

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