Def BigOperators.delabFinsetSum

Modification history

2024-05-28 08:12
Mathlib/Algebra/BigOperators/Basic.lean
chore(Mathlib/Algebra/BigOperators/Basic): unscope `∑ x ∈ s, f x` notations (#13271) …
Modified BigOperators.delabFinsetSumView on Github →
2024-04-09 03:53
Mathlib/Algebra/BigOperators/Basic.lean
fix: add missing withOverApps (#12022) …
Modified BigOperators.delabFinsetSumView on Github →
2023-05-03 23:01
Mathlib/Algebra/BigOperators/Basic.lean
feat: delaborators for Finset.prod and Finset.sum (#3772) …
Added BigOperators.delabFinsetSumView on Github →