Commit 2025-05-14 12:37 79c1c03f

View on Github →

feat: s \ {a ∈ s | p a} = {a ∈ s | ¬ p a} (#24888) I wrote this for #22974, but it isn't needed there in the end.

Estimated changes