Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-21 11:28 233eff0d

View on Github →

feat(data/fintype/card_embedding): the birthday problem (#7363)

Estimated changes

Created archive/100-theorems-list/93_birthday_problem.lean

added theorem birthday

Modified docs/100.yaml

Modified src/data/equiv/basic.lean

added def equiv.subtype_prod_equiv_sigma_subtype

Created src/data/equiv/embedding.lean

added def equiv.cod_restrict

added def equiv.prod_embedding_disjoint_equiv_sigma_embedding_restricted

added def equiv.sum_embedding_equiv_prod_embedding_disjoint

added def equiv.sum_embedding_equiv_sigma_embedding_restricted

added def equiv.unique_embedding_equiv_result

Modified src/data/fintype/basic.lean

added theorem function.embedding.is_empty_of_card_lt

Created src/data/fintype/card_embedding.lean

added theorem fintype.card_embedding

added theorem fintype.card_embedding_eq_if

added theorem fintype.card_embedding_eq_infinite

added theorem fintype.card_embedding_eq_zero

added theorem fintype.card_embedding_of_unique

Modified src/data/nat/factorial.lean

added theorem nat.desc_fac_of_sub

Modified src/logic/embedding.lean

added def equiv.embedding_congr

added theorem equiv.embedding_congr_apply_trans

added theorem equiv.embedding_congr_refl

added theorem equiv.embedding_congr_symm

added theorem equiv.embedding_congr_trans

added def equiv.subtype_injective_equiv_embedding

added theorem function.embedding.mk_coe

Modified src/ring_theory/polynomial/pochhammer.lean