eval_comp_toMvPolynomial — Mathlib

English

The algebra evaluation after composing with the univariate embedding equals performing an aeval with the corresponding image value.

Русский

После композиции с однородным вложением алгебраическое оценивание эквивалентно применению aeval к соответственному значению.

LaTeX

$$$(\mathrm{aeval}\;f) \circ (\mathrm{toMvPolynomial}\;i) = \mathrm{aeval}(f(i))$$$

Lean4

@[simp]
theorem eval_comp_toMvPolynomial (f : σ → R) (i : σ) :
    (eval f).comp (toMvPolynomial (R := R) i) = Polynomial.evalRingHom (f i) := by ext <;> simp

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