map_ofNat — Mathlib

English

For all f ∈ F and n ∈ ℕ with n ≥ 2, f(ofNat(n)) = f(0) + ofNat(n).

Русский

Для любого f ∈ F и n ∈ ℕ с n ≥ 2: f(ofNat(n)) = f(0) + ofNat(n).

LaTeX

$$$\\forall f \\in F,\\forall n \\in \\mathbb{N},\\ [n \\ge 2] \\Rightarrow f(\\operatorname{ofNat}(n)) = f(0) + \\operatorname{ofNat}(n)$$$

Lean4

theorem map_ofNat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ)
    [n.AtLeastTwo] : f ofNat(n) = f 0 + ofNat(n) :=
  map_nat f n

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