English
For a suitable map f, f(ofNat(n)) equals OfNat.ofNat(n) for all natural n.
Русский
Для подходящего отображения f выполняется f(ofNat(n)) = OfNat.ofNat(n) для всех n.
LaTeX
$$$ f(\operatorname{ofNat}(n)) = \operatorname{OfNat}(n) $$$
Lean4
/-- This lemma is not marked `@[simp]` lemma because its `#discr_tree_key` (for the LHS) would just
be `DFunLike.coe _ _`, due to the `ofNat` that https://github.com/leanprover/lean4/issues/2867
forces us to include, and therefore it would negatively impact performance.
If that issue is resolved, this can be marked `@[simp]`. -/
theorem map_ofNat [FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) [Nat.AtLeastTwo n] :
(f ofNat(n) : S) = OfNat.ofNat n :=
map_natCast f n
