Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-25 15:26 0ad5abc7

View on Github →

chore(data/set/finite): golf 2 proofs (#8862) Also add finset.coe_emb.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.coe_coe_emb

added def finset.coe_emb

Modified src/data/set/finite.lean

added theorem set.subset_to_finset_iff