Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.to_finset_univ

Modification history

2023-01-06 22:53
src/data/fintype/basic.lean
feat(data/set/finite): Align `set.to_finset` and `set.finite.to_finset` (#17959) …
Modified set.to_finset_univView on Github →
2022-05-23 12:13
src/data/fintype/basic.lean
refactor(data/set/finite): reorganize and put emphasis on fintype instances (#14136) …
Modified set.to_finset_univView on Github →
2022-02-09 11:36
src/data/fintype/basic.lean
chore(data/fintype/basic): documenting elaboration bug (#11247) …
Modified set.to_finset_univView on Github →
2022-01-04 18:47
src/data/fintype/basic.lean
chore(data/fintype/basic): set.to_finset_univ generalization (#11174)
Modified set.to_finset_univView on Github →
2020-04-30 18:20
src/data/fintype/basic.lean
feat(*): small additions that prepare for Chevalley-Warning (#2560) …
Added set.to_finset_univView on Github →