Theorem Finset.notMem_sdiff_of_mem_right

Modification history

2025-08-03 23:41

Mathlib/Data/Finset/SDiff.lean

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

Modified Finset.notMem_sdiff_of_mem_right View on Github →

2025-05-25 12:30

Mathlib/Data/Finset/SDiff.lean

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

Added Finset.notMem_sdiff_of_mem_right View on Github →