Theorem Ordinal.opow_limit
Modification history
2025-07-11 17:39
Mathlib/SetTheory/Ordinal/Exponential.lean
refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643) …
Modified Ordinal.opow_limitView on Github →2025-01-30 00:35
Mathlib/SetTheory/Ordinal/Exponential.lean
chore(SetTheory/Ordinal/Exponential): redefine ordinal exponential without `bsup` (#19145) …
Modified Ordinal.opow_limitView on Github →