Theorems · Theorem · real analysis
ENNReal.zero_div
∀ {a : ENNReal}, 0 / a = 0- Defined in
- Mathlib.Data.ENNReal.Inv
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- MulZeroClass.zero_mulproof · cited by 1,625
Cited by24
Results whose statement or proof uses this declaration.
- ENNReal.div_le_of_le_mulproof · cited by 10
- Asymptotics.isLittleOTVS_oneproof · cited by 4
- egauge_ball_le_of_one_lt_normproof · cited by 4
- MeasureTheory.Measure.hausdorffMeasure_zero_or_topproof · cited by 3
- ContractingWith.eq_or_edist_eq_top_of_fixedPointsproof · cited by 3
- MeasureTheory.MemLp.norm_rpow_divproof · cited by 2
- MeasureTheory.MemLp.enorm_rpow_divproof · cited by 2
- thickenedIndicatorAux_oneproof · cited by 2
- ZLattice.covolume.tendsto_card_le_div'proof · cited by 1
- ProbabilityTheory.Kernel.setIntegral_densityProcess_of_memproof · cited by 1
- ENNReal.div_div_cancel'proof · cited by 1
- MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_oneproof · cited by 1