mathlib3 documentation

mathlib-archive / wiedijk_100_theorems.birthday_problem

Birthday Problem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves Theorem 93 from the 100 Theorems List.

As opposed to the standard probabilistic statement, we instead state the birthday problem in terms of injective functions. The general result about fintype.card (α ↪ β) which this proof uses is fintype.card_embedding_eq.

theorem theorems_100.birthday  :

Birthday Problem: set cardinality interpretation.

Birthday Problem: first probabilistic interpretation.