Theorem Set.toFinset_nontrivial

Modification history

2025-02-17 17:27
Mathlib/Data/Fintype/Basic.lean
chore(Data/Fintype): split `Data/Fintype/Basic.lean` (#21831) …
Modified Set.toFinset_nontrivialView on Github →
2025-02-12 23:13
Mathlib/Data/Fintype/Basic.lean
feat(Finset): toFinset + nontrivial (#21695) …
Added Set.toFinset_nontrivialView on Github →