Commit 2026-05-21 17:15 785a6a40

View on Github →

chore: use x + 1 instead of succ x in Ordinal.limitRecOn (#39648) The idea is to phase out the use of Order.succ on ordinals. See also Zulip.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.add_mul_add_one

modified theorem Ordinal.add_mul_succ

added theorem Ordinal.limitRecOn_add_one

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/ZFC/VonNeumann.lean