Commit 2026-05-13 09:39 228b412a

View on Github →

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

Estimated changes

added theorem Ordinal.div_eq
added theorem Ordinal.div_eq_iff'
added theorem Ordinal.div_eq_iff
added theorem Ordinal.div_eq_one_iff
modified theorem Ordinal.le_of_dvd