Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-16 18:35 9282f6cd

View on Github →

feat(finset): two simple lemmas (#5387) also open function namespace

Estimated changes

modified theorem finset.coe_injective
added theorem finset.mem_insert_coe
added theorem list.to_finset_surj_on
modified theorem list.to_finset_surjective