Commit 2025-09-01 08:25 12d4fd9b

View on Github →

feat(ENNReal): min x y = 0 ↔ x = 0 ∨ y = 0 and other lemmas (#29165)

Estimated changes

Modified Mathlib/Analysis/Normed/Lp/ProdLp.lean

Modified Mathlib/Data/ENNReal/Basic.lean

added theorem ENNReal.min_eq_zero_iff

Modified Mathlib/Data/ENNReal/Real.lean

added theorem ENNReal.ofReal_max

added theorem ENNReal.ofReal_min

added theorem ENNReal.ofReal_mono