Theorem Ordinal.zero_opow_le

Modification history

2025-01-30 00:35
Mathlib/SetTheory/Ordinal/Exponential.lean
chore(SetTheory/Ordinal/Exponential): redefine ordinal exponential without `bsup` (#19145) …
Added Ordinal.zero_opow_leView on Github →