Theorem NNReal.summable_coe

Modification history

2025-10-06 12:30

Mathlib/Topology/Instances/NNReal/Lemmas.lean

feat(Topology/Algebra/InfiniteSum): generalise to allow summation filters (#29914) …

Modified NNReal.summable_coe View on Github →

2023-03-07 06:34

Mathlib/Topology/Instances/NNReal.lean

feat: port Topology.Instances.NNReal (#2672)

Added NNReal.summable_coe View on Github →