Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 14:40 4eb76a7b

View on Github →

refactor(set_theory/ordinal/arithmetic): Rename theorems to match nat.log API (#12733) We match the API for ordinal.log with that of nat.log.

Estimated changes

Modified src/set_theory/ordinal/arithmetic.lean

deleted theorem ordinal.le_log

modified def ordinal.log

deleted theorem ordinal.log_le_log

deleted theorem ordinal.log_lt

added theorem ordinal.log_mono_right

deleted theorem ordinal.log_not_one_lt

added theorem ordinal.log_of_left_le_one

added theorem ordinal.log_of_not_one_lt_left

deleted theorem ordinal.log_one

added theorem ordinal.log_one_left

added theorem ordinal.log_one_right

deleted theorem ordinal.log_zero

added theorem ordinal.log_zero_left

added theorem ordinal.log_zero_right

added theorem ordinal.lt_opow_iff_log_lt

deleted theorem ordinal.lt_opow_succ_log

added theorem ordinal.lt_opow_succ_log_self

modified theorem ordinal.mod_opow_log_lt_self

added theorem ordinal.opow_le_iff_le_log

deleted theorem ordinal.opow_log_le

added theorem ordinal.opow_log_le_self

modified theorem ordinal.opow_mul_add_pos

added theorem ordinal.zero_le_one

Modified src/set_theory/ordinal/principal.lean