Commit 2024-08-19 00:00 5315a730

View on Github →

chore: protect Finset.ext_iff (#15698) This replaces the manual implementation by one generated by the ext attribute for consistency.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

Modified Mathlib/Data/Finset/Basic.lean

modified theorem Finset.Finset.filter_inj'

modified theorem Finset.Finset.filter_inj

modified theorem Finset.ext

deleted theorem Finset.ext_iff

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Sum.lean

modified theorem Finset.disjSum_eq_empty

Modified Mathlib/Data/Fintype/Basic.lean

modified theorem Finset.eq_univ_iff_forall

Modified Mathlib/Order/Interval/Finset/Basic.lean