Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 23:45 cac4e196

View on Github →

feat(set_theory/ordinal_arithmetic): Proved characterization of log (#11192) As well as a few simple missing lemmas.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.le_mul_left

added theorem ordinal.le_mul_right

added theorem ordinal.log_one

added theorem ordinal.log_power

added theorem ordinal.log_power_mul_add

added theorem ordinal.lt_one_iff_zero

added theorem ordinal.power_mul_add_lt_power_mul_succ

added theorem ordinal.power_mul_add_lt_power_succ

added theorem ordinal.power_mul_add_pos