Theorem ENNReal.toReal_top

Modification history

2026-09-17 17:14
Mathlib/Basic/ENNReal/Basic.lean
feat(Tactic): general tactic to translate `(E)NNReal`, `ENat`, `PNat` goals to `Real` and `Nat` (#43254) …
Modified ENNReal.toReal_topView on Github →
2025-03-20 20:33
Mathlib/Data/ENNReal/Basic.lean
chore(ENNReal): fix names (#23135) …
Added ENNReal.toReal_topView on Github →