Commit 2022-08-03 06:38 53ab3a54
View on Github →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.