Commit 2025-02-24 09:31 247bbcab

View on Github →

feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) We define the nimber inverse and use it to prove nimbers are a field.

Estimated changes

Modified Mathlib/SetTheory/Nimber/Basic.lean

added theorem Nimber.one_le_iff_ne_zero

Modified Mathlib/SetTheory/Nimber/Field.lean

added theorem Nimber.cons_mem_invSet

added def Nimber.invAux

added theorem Nimber.invAux_mem_invSet_of_lt

added theorem Nimber.invAux_ne_zero

added theorem Nimber.invAux_not_mem_invSet

added def Nimber.invSet

added theorem Nimber.invSet_recOn

added theorem Nimber.inv_eq_invAux

added theorem Nimber.mem_invSet_of_lt_invAux

added theorem Nimber.mul_invAux_cancel

added theorem Nimber.zero_mem_invSet