Mathlib Map

Theorems · Theorem · real analysis

NNReal.coe_natCast

∀ (n : ℕ), ↑↑n = ↑n
Defined in
Mathlib.Data.NNReal.Defs
Cited by
34 results in Mathlib
Foundations
Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

EisensteinSeries.norm_eq_max_natAbs · cited by 8EisensteinSeries.norm_eq_…Real.toNNReal_natCast · cited by 7Real.toNNReal_natCastNNReal.natCast_natAbs · cited by 3NNReal.natCast_natAbsNumberField.HeightOneSpectrum.embedding_mul_absNorm · cited by 3HeightOneSpectrum.embeddi…Real.dimH_ball_pi · cited by 2Real.dimH_ball_pivolume_iUnion_setOfPred_liouvilleWith · cited by 2volume_iUnion_setOfPred_l…NNReal.mk_natCast · cited by 2NNReal.mk_natCastNumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd · cited by 2hermiteTheorem.minkowskiB…Complex.nnnorm_natCast · cited by 2Complex.nnnorm_natCastMeasureTheory.lpNorm_nsmul · cited by 2MeasureTheory.lpNorm_nsmulReal.toNNReal_eq_natCast · cited by 2Real.toNNReal_eq_natCastNumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr · cited by 2NumberField.exists_ne_zer…MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part · cited by 1Submartingale.mul_lintegr…MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le · cited by 1StronglyMeasurable.exists…BoxIntegral.HasIntegral.of_aeEq_zero · cited by 1HasIntegral.of_aeEq_zeroReal · cited by 25697RealNNReal · cited by 4310NNRealNNReal.toReal · cited by 1260NNReal.toRealmap_natCast · cited by 134map_natCastNNReal.toRealHom · cited by 13NNReal.toRealHomNNReal.coe_natCastCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by34

Results whose statement or proof uses this declaration.