Commit 2020-05-09 17:40 20c74188

View on Github →

chore(data/finset): drop to_set, use has_lift instead (#2629) Also cleanup coe_to_finset lemmas. Now we have set.finite.coe_to_finset and set.coe_to_finset.

Estimated changes

Modified src/algebra/direct_sum.lean

Modified src/data/finset.lean

added theorem finset.coe_injective

deleted def finset.to_set

deleted theorem finset.to_set_injective

deleted theorem finset.to_set_sdiff

Modified src/data/finsupp.lean

Modified src/data/fintype/basic.lean

added theorem set.coe_to_finset

Modified src/data/set/finite.lean

modified theorem finset.coe_preimage

deleted theorem finset.coe_to_finset'

deleted theorem finset.coe_to_finset

modified theorem set.finite.coe_to_finset

Modified src/linear_algebra/basic.lean

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/finsupp.lean

Modified src/ring_theory/adjoin.lean

Modified src/ring_theory/free_comm_ring.lean

Modified src/ring_theory/noetherian.lean

Modified src/set_theory/ordinal.lean