Theorem Ordinal.lt_add_iff_of_isSuccLimit

Modification history

2025-07-19 23:40

Mathlib/SetTheory/Ordinal/Arithmetic.lean

refactor(SetTheory/Ordinal/Arithmetic): redefine subtraction (#26889) …

Added Ordinal.lt_add_iff_of_isSuccLimit View on Github →