mathlib3

4b82074e - chore(set_theory/ordinal/arithmetic): change `0 < x` assumptions to `x ≠ 0` (#15562)

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`.