Commit 2024-11-15 15:18 d91e72c6

View on Github →

feat: a nontrivial finset is nonempty (#19088) ... and make Finset.subset_empty simp, similarly to Set.subset_empty_iff From GrowthInGroups

Estimated changes

modified theorem Finset.subset_empty