Theorem Ordinal.natCast_pow

Modification history

2026-02-09 01:15
Mathlib/SetTheory/Ordinal/Exponential.lean
refactor(SetTheory/Ordinal): introduce `natCast_pow` (#34662) …
Added Ordinal.natCast_powView on Github →