Commit 2025-01-12 21:12 607d7980

View on Github →

refactor(SetTheory/Ordinal/NaturalOps): redefine natural addition without blsub (#19236) This is progress towards deprecating Ordinal.blsub (and Ordinal.lsub) altogether.

Estimated changes

Modified Mathlib/SetTheory/Game/Birthday.lean

modified theorem SetTheory.PGame.birthday_add

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.iSup_succ

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Ordinal.Iio_one_default_eq

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

deleted theorem Ordinal.nadd_def

modified theorem Ordinal.nadd_one

modified theorem Ordinal.nadd_zero