Commit 2022-07-22 09:11 4b82074e

View on Github →

chore(set_theory/ordinal/arithmetic): change 0 < x assumptions to x ≠ 0 (#15562) Converting from h : 0 < x to h : x ≠ 0 is as easy as h.ne', while the other way round requires ordinal.pos_iff_ne_zero.2 h. As such, we prefer the latter form throughout the ordinal logarithm API. We also rename hypotheses like b0 and x0 to more standard names like hb and hx.

Estimated changes

Modified src/set_theory/ordinal/arithmetic.lean

modified theorem ordinal.add_log_le_log_mul

modified theorem ordinal.log_def

modified theorem ordinal.log_mod_opow_log_lt_log_self

modified theorem ordinal.log_of_left_le_one

modified theorem ordinal.log_of_not_one_lt_left

modified theorem ordinal.log_opow_mul_add

modified theorem ordinal.log_pos

modified theorem ordinal.lt_opow_iff_log_lt

modified theorem ordinal.lt_opow_succ_log_self

modified theorem ordinal.mod_opow_log_lt_self

modified theorem ordinal.opow_le_iff_le_log

modified theorem ordinal.opow_log_le_self

modified theorem ordinal.opow_mul_add_pos

modified theorem ordinal.succ_log_def

Modified src/set_theory/ordinal/cantor_normal_form.lean

Modified src/set_theory/ordinal/principal.lean

modified theorem ordinal.mul_eq_opow_log_succ