Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.coe_to_finset

Modification history

2020-05-09 17:40

src/data/set/finite.lean

chore(data/finset): drop `to_set`, use `has_lift` instead (#2629) …

Deleted finset.coe_to_finset View on Github →

2017-12-07 17:22

data/set/finite.lean

feat(data/set/finite): add finite_to_set, finset.coe_to_finset

Added finset.coe_to_finset View on Github →