Theorem Ordinal.div_eq_iff

Modification history

2026-05-13 09:39

Mathlib/SetTheory/Ordinal/Arithmetic.lean

feat(SetTheory/Ordinal/Arithmetic): a few ordinal division lemmas (#36840)

Added Ordinal.div_eq_iff View on Github →