Theorem Ordinal.CNF.coeff_opow_mul_add

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_opow_mul_addView on Github →