Commit 2024-11-15 01:39 7954f737

View on Github →

feat(SetTheory/Nimber/Field): Nimber multiplication (#16877) We define nimber multiplication and prove that nimbers form a domain and a commutative ring. This placed in a separate file from nimber addition so as to not bloat the imports of SetTheory/Game/Nim.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/SetTheory/Game/Nim.lean

Renamed Mathlib/SetTheory/Ordinal/Nimber.lean to Mathlib/SetTheory/Nimber/Basic.lean

added theorem Nimber.lt_one_iff_zero

added theorem Nimber.not_bddAbove_compl_of_small

Created Mathlib/SetTheory/Nimber/Field.lean

added theorem Nimber.exists_of_lt_mul

added theorem Nimber.mul_def

added theorem Nimber.mul_le_of_forall_ne