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
.
feat(Finset): toFinset + nontrivial (#21695)
We add simp lemmas for nontriviality with Set.Finite.toFinset
and Set.toFinset
.