Theorem Finset.insert_sdiff_self_of_mem

Modification history

2025-08-11 13:56
Mathlib/Data/Finset/SDiff.lean
feat(Finset): `insert a (s \ {a}) = s` if `a ∈ s` (#28172) …
Added Finset.insert_sdiff_self_of_memView on Github →