Theorems · Theorem · commutative algebra

map_ofNat

∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo],
  f (OfNat.ofNat n) = OfNat.ofNat n

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].

Defined in

Mathlib.Data.Nat.Cast.Basic

Cited by

73 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

NonAssocSemiringNonAssocSemiringFunLikeRingHomClassNat.AtLeastTwo