Commit 2026-02-23 17:11 cfc99f1a

View on Github →

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

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.isSuccLimit_mul

added theorem Ordinal.isSuccLimit_mul_right

modified theorem Ordinal.isSuccLimit_sub

added theorem Ordinal.isSuccPrelimit_iff_omega0_dvd

added theorem Ordinal.isSuccPrelimit_mul_left

added theorem Ordinal.isSuccPrelimit_mul_right

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean