eval₂_natCast — Mathlib

English

The evaluation at a natural number embedded into the polynomial ring equals that natural number's image under the scalar map.

Русский

Оценивание натурального числа, встроенного в кольцо полиномов, равняется образу этого числа под скаляровой картой.

LaTeX

$$$\mathrm{eval_2}(n) = n$ (via the natural cast)$$

Lean4

@[simp]
theorem eval₂_natCast (n : Nat) : (n : MvPolynomial σ R).eval₂ f g = n :=
  (eval₂_C _ _ _).trans (map_natCast f n)

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