Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-26 17:00 b67044ba

View on Github →

feat(set_theory/ordinal/arithmetic): miscellaneous arithmetic lemmas (#15990) Will be used to prove statements about the Cantor Normal Form.

Estimated changes

Modified src/set_theory/ordinal/arithmetic.lean

modified theorem ordinal.add_sub_add_cancel

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 src/set_theory/ordinal/exponential.lean

added theorem ordinal.div_opow_log_pos

modified theorem ordinal.opow_dvd_opow

modified theorem ordinal.opow_dvd_opow_iff

Modified src/set_theory/ordinal/notation.lean