Commit 2025-02-12 23:13 589e8608

View on Github →

feat(Finset): toFinset + nontrivial (#21695) We add simp lemmas for nontriviality with Set.Finite.toFinset and Set.toFinset.

Estimated changes