map_ofNat — Mathlib

English

If n is a natural number with at least two, map f of_nat n equals the same natural number as n: (ofNat n).map f = ofNat n.

Русский

Для натурального числа n, удовлетворяющего условию, map f (ofNat n) = ofNat n.

LaTeX

$$$$\operatorname{map} f\bigl(\mathrm{ofNat}(n)\bigr) = \mathrm{ofNat}(n).$$$$

Lean4

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

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