Commit 2023-03-27 15:24 b8f01542

View on Github →

feat: forward-port #15990 (#3120)

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.mod_le

added theorem Ordinal.mod_mod

added theorem Ordinal.mod_mod_of_dvd

added theorem Ordinal.mul_add_mod_self

added theorem Ordinal.mul_mod

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

added theorem Ordinal.div_opow_log_pos

modified theorem Ordinal.opow_dvd_opow