Commit 2024-10-04 21:26 d2499a7b

View on Github →

feat (Mathlib/SetTheory/Ordinal/Arithmetic): add bounded recursion on ordinals (#16663) Add a recursion principal defining functions with domain Iio o for an ordinal o.

Estimated changes