Theorem Finset.insert_erase
Modification history
2026-08-12 08:59
Mathlib/Data/Finset/Basic.lean
feat(Data/Finset): `insert a (s.erase a) = insert a s` (#40775)
Modified Finset.insert_eraseView on Github →2025-12-08 16:53
Mathlib/Data/Finset/Basic.lean
chore(Data/Finset/Basic): use more dot notation in `Data.Finset.Basic` (#31838)
Modified Finset.insert_eraseView on Github →2025-08-03 23:41
Mathlib/Data/Finset/Basic.lean
feat: start adding `@[grind]` annotations for `Finset` (#27818) …
Modified Finset.insert_eraseView on Github →