Theorem Ordinal.isSuccPrelimit_mul_left

Modification history

2026-02-23 17:11

Mathlib/SetTheory/Ordinal/Arithmetic.lean

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

Added Ordinal.isSuccPrelimit_mul_left View on Github →