Theorem Nimber.one_le_iff_ne_zero

Modification history

2025-02-24 09:31

Mathlib/SetTheory/Nimber/Basic.lean

feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) …

Added Nimber.one_le_iff_ne_zero View on Github →