Theorem Ordinal.CNF.coeff_of_le_one

Modification history

2025-08-20 19:33
Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
feat: Cantor normal form as a finitely supported function (#28586)
Added Ordinal.CNF.coeff_of_le_oneView on Github →