Revision #3563 → #4111 · back to history
modifiedPigeonhole boundfab3b419e178
| Field | From #3563 | To #4111 |
|---|
| mathlib.module | Mathlib.Data.Finset.Basic | Mathlib.Data.Finset.Card |
| note | Mathlib formalizes the pigeonhole principle in general (e.g. `Finset.exists_ne_map_eq_of_card_lt_of_maps_to`), but the birthday-specific consequence is not stated. | Mathlib formalizes the pigeonhole principle in general (e.g. `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` in `Mathlib.Data.Finset.Card`), but the birthday-specific consequence is not stated. |
modifiedUpper bound via Halmos argumentee2485100f75
| Field | From #3563 | To #4111 |
|---|
| kind | theorem | proposition |
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Exp | Mathlib.Analysis.Complex.Exponential |
addedLinearity of expectation for indicatorsf57f15a405fe
addedHarmonic number formula nH_nef617c2ecab7