Theorems · Theorem · commutative algebra
ENNReal.toReal_smul
∀ (r : NNReal) (s : ENNReal), (r • s).toReal = r • s.toReal
- Defined in
- Mathlib.Data.ENNReal.Action
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- ENNRealstatement and proof · cited by 9,879
- NNRealstatement and proof · cited by 4,310
- ENNReal.ofNNRealproof · cited by 1,279
- NNReal.toRealproof · cited by 1,260
- ENNReal.toRealstatement and proof · cited by 859
- smul_eq_mulproof · cited by 357
- ENNReal.toReal_mulproof · cited by 57
- ENNReal.smul_defproof · cited by 22
- ENNReal.coe_toRealproof · cited by 14
Cited by3
Results whose statement or proof uses this declaration.
- infDist_smul₀proof · cited by 1
- MeasureTheory.smul_le_stoppedValue_hittingBtwnproof · cited by 1
- diam_smul₀proof · cited by 0