Commit 2026-02-27 10:47 3d588181

View on Github →

refactor: nicer definition for ordinal division (#35849) By leveraging the API on Order.IsNormal, we can define ordinal division in a way that almost immediately proves the characterizing Galois connection. (We also remove a redundant expose in a file with no defs.)

Estimated changes

Modified Mathlib/Order/IsNormal.lean

added theorem Order.IsNormal.le_iff_le_sSup'

added theorem Order.IsNormal.le_iff_le_sSup

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Ordinal.div_le

modified theorem Ordinal.div_zero

modified theorem Ordinal.le_div

added theorem Ordinal.lt_mul_iff_div_lt

added theorem Ordinal.mul_div_gc

added theorem Ordinal.mul_le_iff_le_div

modified theorem Ordinal.mul_sub

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean