Skip to content

Commit 85d7017

Browse files
Ruben-VandeVeldeRuben-VandeVelde
committed
chore: enable assert_not_exists in BigOperators (leanprover-community#33187)
1 parent d2cd533 commit 85d7017

2 files changed

Lines changed: 2 additions & 3 deletions

File tree

‎Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ In this file we prove theorems about products and sums indexed by a `Finset`.
1717

1818
@[expose] public section
1919

20-
-- TODO: assert_not_exists AddCommMonoidWithOne
20+
assert_not_exists AddCommMonoidWithOne
2121
assert_not_exists MonoidWithZero MulAction IsOrderedMonoid
2222
assert_not_exists Finset.preimage Finset.sigma Fintype.piFinset
2323
assert_not_exists Finset.piecewise Set.indicator MonoidHom.coeFn Function.support IsSquare

‎Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,8 +44,7 @@ See the documentation of `to_additive.attr` for more information.
4444

4545
@[expose] public section
4646

47-
-- TODO
48-
-- assert_not_exists AddCommMonoidWithOne
47+
assert_not_exists AddCommMonoidWithOne
4948
assert_not_exists MonoidWithZero
5049
assert_not_exists MulAction
5150
assert_not_exists IsOrderedMonoid

0 commit comments

Comments
 (0)