Theorem Nimber.mem_invSet_of_lt_invAux

Modification history

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