[Merged by Bors] - feat(SetTheory/Game/Birthday): Define birthday of a game#15716
[Merged by Bors] - feat(SetTheory/Game/Birthday): Define birthday of a game#15716
Conversation
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
PR summary 682211c9d9
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.SetTheory.Game.Birthday | 629 | 630 | +1 (+0.16%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Birthday |
1 |
Declarations diff
+ birthday
+ birthday_add_le
+ birthday_eq_pGameBirthday
+ birthday_eq_zero
+ birthday_natCast
+ birthday_ofNat
+ birthday_one
+ birthday_ordinalToGame
+ birthday_ordinalToPGame
+ birthday_quot_le_pGameBirthday
+ birthday_star
+ birthday_sub
+ birthday_sub_le
+ birthday_zero
+ le_birthday
+ neg_birthday_le
+ quot_natCast
+ toGame_natCast
+ toPGame_natCast
+ zero_def
++ birthday_neg
- birthday_add_nat
- birthday_add_one
- birthday_add_zero
- birthday_nat_add
- birthday_nat_cast
- birthday_one_add
- birthday_zero_add
- neg_birthday
- toPGame_birthday
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Eric's comment having been addressed, maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
The updated module description explains how this differs from the birthday of a pre-game.
|
Pull request successfully merged into master. Build succeeded: |
The updated module description explains how this differs from the birthday of a pre-game.