Commit 2024-10-10 11:56 f13b8bf8

View on Github →

feat(SetTheory/Ordinal/Nimber): nim addition of natural numbers is XOR (#16878) We also introduce the notation ∗o for Ordinal.toNimber o. Note that for n : ℕ, ∗n is not the same as NatCast, as e.g. ∗2 ≠ ↑2 = 0.

Estimated changes

added theorem Nimber.add_nat
modified theorem Nimber.succ_def
modified theorem Nimber.toOrdinal_eq_one
modified theorem Nimber.toOrdinal_eq_zero
modified theorem Nimber.toOrdinal_max
modified theorem Nimber.toOrdinal_min
modified theorem Nimber.toOrdinal_toNimber
modified theorem Ordinal.toNimber_eq_one
modified theorem Ordinal.toNimber_eq_zero
modified theorem Ordinal.toNimber_max
modified theorem Ordinal.toNimber_min
modified theorem Ordinal.toNimber_one
modified theorem Ordinal.toNimber_toOrdinal
modified theorem Ordinal.toNimber_zero