Theorem ENNReal.ofNat_lt_top

Modification history

2025-01-02 08:45

Mathlib/Data/ENNReal/Basic.lean

chore: use `ofNat()` around `Real` and `Complex` (#20388) …

Modified ENNReal.ofNat_lt_top View on Github →

2024-10-29 07:44

Mathlib/Data/ENNReal/Basic.lean

feat(Tactic): add `finiteness` tactic (#18034) …

Added ENNReal.ofNat_lt_top View on Github →