Skip to content

[Merged by Bors] - fix(Algebra/BigOperators/Group/Finset): Add missing binder annotation with pp.analyze in Finset.sum#33070

Closed
MrQubo wants to merge 3 commits intoleanprover-community:masterfrom
MrQubo:pp-analyze-finset-sum
Closed

[Merged by Bors] - fix(Algebra/BigOperators/Group/Finset): Add missing binder annotation with pp.analyze in Finset.sum#33070
MrQubo wants to merge 3 commits intoleanprover-community:masterfrom
MrQubo:pp-analyze-finset-sum

Commits

Commits on Dec 19, 2025