Theorem Ordinal.CNF.coeff_eq_zero_of_lt

Modification history

2026-03-02 16:30

Mathlib/SetTheory/Ordinal/CantorNormalForm.lean

feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF (#33840) …

Added Ordinal.CNF.coeff_eq_zero_of_lt View on Github →