Theorem WithTop.sum_lt_top_iff
Modification history
2024-08-27 20:26
Mathlib/Algebra/BigOperators/WithTop.lean
feat(NNReal/ENNReal): More basic lemmas (#16133) …
Deleted WithTop.sum_lt_top_iffView on Github →2024-05-27 08:32
Mathlib/Algebra/BigOperators/WithTop.lean
chore: Use the new `∑ i ∈ s, f i` notation (#13209) …
Modified WithTop.sum_lt_top_iffView on Github →2024-02-12 06:18
Mathlib/Algebra/BigOperators/Order.lean
chore: Split off `WithTop` lemmas (#10239) …
Modified WithTop.sum_lt_top_iffView on Github →