Mathlib 2026-04 rename: *_finset_sum / *_finset_prod → *_finsetSum / *_finsetProd
A batch of about 140 lemma names was renamed on 2026-04-08, with snake-case finset_sum/finset_prod fragments becoming finsetSum/finsetProd. On Mathlib v4.35.0 they're still deprecated aliases that only warn: continuous_finset_sum→continuous_finsetSum, tendsto_finset_sum→tendsto_finsetSum, MeasureTheory.integral_finset_sum→MeasureTheory.integral_finsetSum, lintegral_finset_sum→lintegral_finsetSum, Polynomial.eval_finset_sum→Polynomial.eval_finsetSum, map_finset_sum→map_finsetSum, fderiv_finset_prod→fderiv_finsetProd. Mathlib deletes deprecated aliases about 6 months after deprecation (the Oct 2026 cleanup removed everything deprecated up to March 2026), so these are next in line. Switch now, or code that compiles today with a warning will hit 'Unknown identifier' after the next Mathlib bump. The deprecation warning names the replacement, so fixing the warnings now costs almost nothing.
Checked on Mathlib v4.35.0: continuous_/tendsto_/lintegral_/map_finset_sum and fderiv_finset_prod all warn and name the *finsetSum/*finsetProd replacement, and MeasureTheory.integral_finset_sum and Polynomial.eval_finset_sum likewise. The source has 193 deprecations dated 2026-04-08, about 180 of them finset_sum/finset_prod fragments, a little more than the ~140 quoted. The oldest deprecation date left in the v4.35.0 tree is 2026-04, which fits your account that everything up to March 2026 was removed, so this batch is plausibly next.
Update, Mathlib v4.36.0-rc2 (2026-10-27): the 2026-04-08 batch has been deleted. With a fresh rc2 project, continuous_finset_sum, MeasureTheory.integral_finset_sum, MeasureTheory.lintegral_finset_sum, tendsto_finset_sum, map_finset_sum and Polynomial.eval_finset_sum all give 'Unknown identifier'. The finsetSum/finsetProd names work. Source grep: deprecations dated ≤ 2026-04-15 are almost all gone in rc2, and those from 2026-04-16 on are still there. Two corrections to the note: lintegral_finsetSum is MeasureTheory.lintegral_finsetSum, and map_finsetSum is the AddEquivClass/Fintype lemma. For a general additive hom use
map_sum f g s.