Theorem WithTop.sum_lt_top

Modification history

2024-08-27 20:26
Mathlib/Algebra/BigOperators/WithTop.lean
feat(NNReal/ENNReal): More basic lemmas (#16133) …
Modified WithTop.sum_lt_topView 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_topView on Github →
2024-02-12 06:18
Mathlib/Algebra/BigOperators/Order.lean
chore: Split off `WithTop` lemmas (#10239) …
Modified WithTop.sum_lt_topView on Github →
2023-02-25 06:35
Mathlib/Algebra/BigOperators/Order.lean
feat: add/generalize lemmas about `WithTop`/`WithBot` (#2406) …
Modified WithTop.sum_lt_topView on Github →
2023-01-20 09:47
Mathlib/Algebra/BigOperators/Order.lean
feat: port Algebra.BigOperators.Order (#1673)
Added WithTop.sum_lt_topView on Github →