Commit 2025-01-30 00:35 8ec167c6

View on Github →

chore(SetTheory/Ordinal/Exponential): redefine ordinal exponential without bsup (#19145) Ordinal.bsup is planned to be deprecated.

Estimated changes

deleted theorem Ordinal.opow_def
modified theorem Ordinal.opow_limit
modified theorem Ordinal.opow_succ
modified theorem Ordinal.zero_opow'
added theorem Ordinal.zero_opow_le