Commit 2023-06-17 07:20 fb57439a

View on Github →

feat: add lemmas about ENNReals (#5084) Also correct some simps. Partially forward-port leanprover-community/mathlib#18731

Estimated changes

Modified Mathlib/Analysis/MeanInequalitiesPow.lean

Modified Mathlib/Data/Real/ENNReal.lean

deleted theorem ENNReal.div_eq_inv_mul

added theorem ENNReal.toNNReal_ne_one

added theorem ENNReal.toNNReal_ne_zero

added theorem ENNReal.toReal_ne_one

added theorem ENNReal.toReal_ne_zero

Modified Mathlib/MeasureTheory/Function/L1Space.lean