Theorem Ordinal.natCast_image_Iio

Modification history

2026-04-02 20:16
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat: lemmas on ordinal `Nat.cast` (#36584) …
Added Ordinal.natCast_image_IioView on Github →