Commit 2025-10-15 08:28 30887119

View on Github →

feat: {x | p x}⁻¹ = {x | p x⁻¹} (#30487)

Estimated changes

added theorem Finset.inv_filter
added theorem Finset.inv_filter_univ
added theorem Set.inv_setOf