Commit 2025-01-30 19:51 e4f90bc8

chore: deprecate the ∑ x in s, f x notation (#21253) Make the ∑ x in s, f x and ∑ x : ty in s, f x syntaxes print a code action suggesting to replace to ∑ x ∈ s, f x. This makes the old syntaxes noisy and therefore unusable in mathlib. Therefore, we must also replace the last few uses of the old syntaxes by the new one.