Theorem Ordinal.add_mul_add_one

Modification history

2026-05-21 17:15
Mathlib/SetTheory/Ordinal/Arithmetic.lean
chore: use `x + 1` instead of `succ x` in `Ordinal.limitRecOn` (#39648) …
Added Ordinal.add_mul_add_oneView on Github →