Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-18 22:20 5a017443

View on Github →

feat(data/{finset,set}/basic): insert a s = s ↔ a ∈ s (#15493) and s.erase a = s ↔ a ∉ s.

Estimated changes