Theorem EReal.add_ne_top_iff_of_ne_bot

Modification history

2025-08-14 21:52
Mathlib/Data/EReal/Operations.lean
chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (#28424)
Deleted EReal.add_ne_top_iff_of_ne_botView on Github →
2025-03-31 03:39
Mathlib/Data/EReal/Basic.lean
chore: split `Data.EReal.Basic` (#23428) …
Modified EReal.add_ne_top_iff_of_ne_botView on Github →
2025-01-13 10:36
Mathlib/Data/Real/EReal.lean
feat(EReal): add `toENNReal` (#18885) …
Added EReal.add_ne_top_iff_of_ne_botView on Github →