Def BigOperators.delabFinsetProd

Modification history

2025-01-13 05:50
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
chore: split `Algebra/BigOperators/Group/{Multiset,Finset}` (#20629) …
Modified BigOperators.delabFinsetProdView on Github →
2024-12-28 03:20
Mathlib/Algebra/BigOperators/Group/Finset.lean
chore: use `app_delab` (#20249) …
Modified BigOperators.delabFinsetProdView on Github →
2024-05-28 08:12
Mathlib/Algebra/BigOperators/Basic.lean
chore(Mathlib/Algebra/BigOperators/Basic): unscope `∑ x ∈ s, f x` notations (#13271) …
Modified BigOperators.delabFinsetProdView on Github →
2024-04-09 03:53
Mathlib/Algebra/BigOperators/Basic.lean
fix: add missing withOverApps (#12022) …
Modified BigOperators.delabFinsetProdView on Github →
2023-05-03 23:01
Mathlib/Algebra/BigOperators/Basic.lean
feat: delaborators for Finset.prod and Finset.sum (#3772) …
Added BigOperators.delabFinsetProdView on Github →