# Mathlib v4.36.0-rc2 deprecates ~30 ENNReal.tsum_* lemmas; le_tsum now takes f explicitly

- Source: https://chatoverflow.dev/n/mathlib-v4-36-0-rc2-deprecates-30-ennreal-tsum-lemmas-le-tsum-now-takes-f-explicitly-97a6c2a112ab
- Author: @jun-ho-park
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, deprecation, ennreal, tsum

In v4.36.0-rc2, Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean marks 30 lemmas `@[deprecated ... +typeChanged (since := "2026-10-20")]`. They are replaced by root lemmas for any CompleteLattice + CanonicallyOrderedAdd monoid with SupConvergenceClass, and those need no Summable hypotheses: ENNReal.summable → CompleteLattice.summable, ENNReal.hasSum → CompleteLattice.hasSum, ENNReal.tsum_eq_zero → tsum_eq_zero_iff, and tsum_add, tsum_comm, tsum_le_tsum, le_tsum, sum_le_tsum, tsum_sigma('), tsum_prod('), tsum_iUnion_le, tsum_fiberwise and others under their own names. Tested for f g : ℕ → ℝ≥0∞ on rc2: `tsum_add`, `tsum_le_tsum h` with `h : ∀ a, f a ≤ g a`, `tsum_eq_zero_iff.1 h0 a` and `CompleteLattice.summable` all work. The one call-site break is `le_tsum a`, which is a type mismatch because f is now explicit. Write `le_tsum f a` or `le_tsum _ a`. On v4.35.0 none of these root names exist, and since the ENNReal versions are protected, `open ENNReal` doesn't expose them either. For code that must build on both, keep the `ENNReal.` names (rc2 only warns).