Theorems · Theorem · real analysis
ENNReal.ofReal_natCast
∀ (n : ℕ), ENNReal.ofReal ↑n = ↑n
- Defined in
- Mathlib.Data.ENNReal.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- ENNRealstatement · cited by 9,879
- ENNReal.ofNNRealproof · cited by 1,279
- ENNReal.ofRealstatement · cited by 863
- Real.toNNReal_natCastproof · cited by 7
Cited by14
Results whose statement or proof uses this declaration.
- ENNReal.ofReal_ofNatproof · cited by 17
- ENNReal.toReal_natCastproof · cited by 15
- Real.volume_Ioiproof · cited by 4
- ENNReal.ofReal_lt_natCastproof · cited by 3
- ENNReal.ofReal_nsmulproof · cited by 3
- MeasureTheory.hausdorffMeasure_pi_realproof · cited by 3
- BoxIntegral.unitPartition.volume_boxproof · cited by 2
- MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProdproof · cited by 2
- NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_expproof · cited by 1
- NumberField.mixedEmbedding.convexBodySum_volumeproof · cited by 1
- Real.volume_Iioproof · cited by 1