mathlib3

53ab3a54 - feat(set_theory/ordinal/arithmetic): generalize `mod_opow_log_lt_self` (#15448)

feat(set_theory/ordinal/arithmetic): generalize `mod_opow_log_lt_self` (#15448) We remove the assumption `b ≠ 0` from `ordinal.mod_opow_log_lt_self`, and from other theorems/definitions that depended on it.