Theorem Finset.eq_of_mem_of_notMem_erase

Modification history

2025-08-03 23:41

Mathlib/Data/Finset/Erase.lean

feat: start adding `@[grind]` annotations for `Finset` (#27818) …

Modified Finset.eq_of_mem_of_notMem_erase View on Github →

2025-05-25 12:30

Mathlib/Data/Finset/Erase.lean

chore(*): not_mem/nmem -> notMem (#25159)

Added Finset.eq_of_mem_of_notMem_erase View on Github →