eval₂_ofNat — Mathlib

English

The natural-number interpreted as a polynomial via OfNat evaluates to the same natural number.

Русский

Число, воспринятое как полином через OfNat, при оценке даёт саму цифру.

LaTeX

$$$\operatorname{ev}_{f,x}\bigl(\mathrm{ofNat}(n)\bigr) = \mathrm{ofNat}(n)$$$

Lean4

@[simp]
theorem eval₂_ofNat {S : Type*} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) :
    (ofNat(n) : R[X]).eval₂ f a = ofNat(n) := by simp [OfNat.ofNat]

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