Commit 2026-02-09 01:15 efc0e39e
View on Github →refactor(SetTheory/Ordinal): introduce natCast_pow (#34662)
We introduce natCast_pow : ↑(m ^ n) = ↑m ^ n for ordinals. We deprecate natCast_opow : ↑(m ^ n) = ↑m ^ ↑n, which aside from being named wrong, has an RHS which is not simp-normal.
See Zulip.