Theorem Ordinal.CNF.coeff_of_not_mem_CNF

Modification history

2026-03-02 16:30
Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF (#33840) …
Deleted Ordinal.CNF.coeff_of_not_mem_CNFView on Github →
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_not_mem_CNFView on Github →