Commit 2026-03-02 16:30 d7da6fe1

View on Github →

feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF (#33840) Used in the CGT repo.

Estimated changes

added theorem Ordinal.CNF.coeff_eval
added theorem Ordinal.CNF.coeff_inj
added def Ordinal.CNF.eval
added theorem Ordinal.CNF.eval_add
added theorem Ordinal.CNF.eval_coeff
added theorem Ordinal.CNF.eval_lt
deleted theorem Ordinal.CNF.lt_snd
added theorem Ordinal.CNF.snd_pos