Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 10:12 0faebd2a

View on Github →

chore(fintype/card_embedding): generalize instances (#12775)

Estimated changes

Modified src/data/fintype/basic.lean

added theorem fintype.card_compl_set

added theorem fintype.card_range

added theorem set.to_finset_compl

Modified src/data/fintype/card_embedding.lean

modified theorem fintype.card_embedding_eq

modified theorem fintype.card_embedding_eq_of_infinite

modified theorem fintype.card_embedding_eq_of_unique

Modified src/data/set/finite.lean

deleted theorem set.to_finset_compl

Modified src/logic/embedding.lean

added def function.embedding.option_embedding_equiv