Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 17:40 a3470769

View on Github →

feat(set_theory/game/birthday): birthday of addition equals natural addition of birthdays (#14549)

Estimated changes

Modified src/order/lattice.lean

added theorem max_max_max_comm

added theorem min_min_min_comm

Modified src/set_theory/game/birthday.lean

added theorem pgame.birthday_add

added theorem pgame.birthday_add_nat

added theorem pgame.birthday_add_one

modified theorem pgame.birthday_add_zero

modified theorem pgame.birthday_eq_zero

added theorem pgame.birthday_nat_add

added theorem pgame.birthday_nat_cast

added theorem pgame.birthday_one_add

modified theorem pgame.birthday_zero_add

modified theorem pgame.neg_birthday_le

Modified src/set_theory/ordinal/arithmetic.lean

added theorem ordinal.lsub_sum

added theorem ordinal.one_add_nat_cast

added theorem ordinal.sup_sum