Theorem ENNReal.tsum_coe_ne_top_iff_summable_coe

Modification history

2026-01-21 17:08

Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean

chore: move tsum lemmas in `ENNReal.Lemmas` to `InfiniteSum.ENNReal` (#34058) …

Modified ENNReal.tsum_coe_ne_top_iff_summable_coe View on Github →

2023-03-10 06:37

Mathlib/Topology/Instances/ENNReal.lean

feat: port Topology.Instances.ENNReal (#2734) …

Added ENNReal.tsum_coe_ne_top_iff_summable_coe View on Github →