Theorem Nimber.invAux_mem_invSet_of_lt

Modification history

2025-02-24 09:31
Mathlib/SetTheory/Nimber/Field.lean
feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) …
Added Nimber.invAux_mem_invSet_of_ltView on Github →