Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.default_coe_singleton

Modification history

2022-01-09 18:06
src/data/set/basic.lean
chore(*): update to 3.37.0c (#11325) …
Modified set.default_coe_singletonView on Github →
2021-04-01 01:24
src/data/set/basic.lean
feat(data/set/basic): default_coe_singleton (#6971)
Added set.default_coe_singletonView on Github →