Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-08 16:26 14a7c39d

View on Github →

chore(data/finset/basic): use has_coe_t for coercion of finset to set (#4917)

Estimated changes

modified theorem finset.coe_empty
modified theorem finset.coe_erase
modified theorem finset.coe_inj
modified theorem finset.coe_inter
modified theorem finset.coe_mem
modified theorem finset.coe_nonempty
modified theorem finset.coe_sdiff
modified theorem finset.coe_singleton
modified theorem finset.coe_ssubset
modified theorem finset.coe_union
modified theorem finset.mem_coe
modified theorem finset.mk_coe
modified theorem finset.piecewise_coe
modified theorem finset.set_of_mem