Commit 2024-09-16 17:23 86a4bd30

View on Github →

feat(SetTheory/Ordinal/Nimber): Initial development of nimbers (#16088) For the moment, we only prove that they form an additive commutative group.

Estimated changes

added theorem Nimber.add_cancel_left
added theorem Nimber.add_def
added theorem Nimber.add_eq_zero
added theorem Nimber.add_ne_zero_iff
added theorem Nimber.add_self
added theorem Nimber.add_trichotomy
added theorem Nimber.bot_eq_zero
added theorem Nimber.induction
added theorem Nimber.lt_wf
added theorem Nimber.succ_def
added def Nimber.toOrdinal
added theorem Nimber.toOrdinal_max
added theorem Nimber.toOrdinal_min
added theorem Nimber.toOrdinal_one
added theorem Nimber.toOrdinal_zero
added def Nimber
added def Ordinal.toNimber
added theorem Ordinal.toNimber_max
added theorem Ordinal.toNimber_min
added theorem Ordinal.toNimber_one
added theorem Ordinal.toNimber_zero
added theorem not_small_nimber