Commit 2025-09-07 08:33 1dbe7a29
View on Github →feat: ∑ i ∈ s with hi : p i, f i hi syntax for big operators (#11563)
Define new notation for Finset.sum/Finset.prod. ∑ i ∈ s with hi : p i, f i hi is now notation for ∑ i ∈ s, if hi : p i then f i hi else 0.