Theorem Ordinal.add_mul_succ

Modification history

2026-05-21 17:15
Mathlib/SetTheory/Ordinal/Arithmetic.lean
chore: use `x + 1` instead of `succ x` in `Ordinal.limitRecOn` (#39648) …
Modified Ordinal.add_mul_succView on Github →
2023-02-16 08:59
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat: port SetTheory.Ordinal.Arithmetic (#2271)
Added Ordinal.add_mul_succView on Github →