eval_ofNat — Mathlib

English

For natural n with AtLeastTwo, eval ofNat(n) equals the corresponding numeral in the target semiring: eval f (ofNat(n)) = ofNat(n).

Русский

Для натурального числа n с условием AtLeastTwo оценка ofNat(n) равна соответствующему числу в целевой полугруппе: eval f (ofNat(n)) = ofNat(n).

LaTeX

$$$\\mathrm{eval} f (\\mathrm{ofNat}(n)) = \\mathrm{ofNat}(n)$$$

Lean4

@[simp]
theorem eval_ofNat (n : Nat) [n.AtLeastTwo] : (ofNat(n) : MvPolynomial σ R).eval f = ofNat(n) :=
  map_ofNat _ n

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