Theorems · Theorem · commutative algebra
eq_natCast
∀ {R : Type u_3} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : FunLike F ℕ R] [RingHomClass F ℕ R] (f : F)
(n : ℕ), f n = ↑n- Defined in
- Mathlib.Data.Nat.Cast.Basic
- Cited by
- 104 results in Mathlib
- Foundations
- Depth 23 from the axioms, rests on 170 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- FunLikestatement and proof · cited by 2,560
- map_oneproof · cited by 861
- NonAssocSemiringstatement and proof · cited by 805
- RingHomClassstatement and proof · cited by 193
- eq_natCast'proof · cited by 2
Cited by104
Results whose statement or proof uses this declaration.
- MeromorphicAt.meromorphicTrailingCoeffAt_smulproof · cited by 7
- SameRay.sameRay_nonneg_smul_rightproof · cited by 6
- RootPairing.setOfPred_root_add_zsmul_eq_Icc_of_linearIndependentproof · cited by 5
- Orientation.rotation_rotationproof · cited by 5
- convex_segmentproof · cited by 5
- AffineSubspace.wOppSide_iff_exists_leftproof · cited by 5
- Wbtw.wOppSide₁₃proof · cited by 4
- ascPochhammer_eval_castproof · cited by 4
- Polynomial.toLaurent_C_mul_Tproof · cited by 4
- RootPairing.chainBotCoeff_sub_chainTopCoeffproof · cited by 4
- Submodule.starProjection_singletonproof · cited by 4
- EuclideanGeometry.mul_dist_eq_abs_sub_sq_distproof · cited by 3