Theorem ENat.toENNReal_eq_zero

Modification history

2026-07-09 14:40
Mathlib/Data/Real/ENatENNReal.lean
feat(MeasureTheory): mass of `count.real` (#40367) …
Added ENat.toENNReal_eq_zeroView on Github →