map_ofNat' — Mathlib

English

For a structure-preserving map f between appropriate types, f(ofNat(n)) equals ofNat(n) for natural numbers n.

Русский

Для отображения, сохраняющего структуру, f(ofNat(n)) = ofNat(n) для натуральных n.

LaTeX

$$$ f(\operatorname{ofNat}(n)) = \operatorname{ofNat}(n) $$$

Lean4

theorem map_ofNat' {A} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) (n : ℕ)
    [n.AtLeastTwo] : f (OfNat.ofNat n) = OfNat.ofNat n :=
  map_natCast' f h n

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