Theorem Ordinal.boundedLimitRec_zero

Modification history

2024-10-04 21:26
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat (Mathlib/SetTheory/Ordinal/Arithmetic): add bounded recursion on ordinals (#16663) …
Added Ordinal.boundedLimitRec_zeroView on Github →