Commit 2026-07-09 14:40 69723202

View on Github →

feat(MeasureTheory): mass of count.real (#40367) From MeanFourier

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Real/ENatENNReal.lean

added theorem ENat.toENNReal_eq_zero

Modified Mathlib/MeasureTheory/Measure/Count.lean

added theorem MeasureTheory.Measure.count_real_univ

Modified Mathlib/RingTheory/Length.lean

Created Mathlib/SetTheory/Cardinal/ENNReal.lean

added theorem ENNReal.toReal_enatCard

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem ENat.card_ne_zero

modified theorem ENat.card_pos