Theorem Ordinal.isSuccLimit_sub

Modification history

2026-02-23 17:11

Mathlib/SetTheory/Ordinal/Arithmetic.lean

feat(SetTheory/Ordinal/Arithmetic): prove `isSuccPrelimit_iff_omega0_dvd` (#34664)

Modified Ordinal.isSuccLimit_sub View on Github →

2025-07-11 17:39

Mathlib/SetTheory/Ordinal/Arithmetic.lean

refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643) …

Added Ordinal.isSuccLimit_sub View on Github →