Commit 2025-08-20 19:33 85988251

View on Github →

feat: Cantor normal form as a finitely supported function (#28586)

Estimated changes

Modified Mathlib/Data/List/AList.lean

added theorem AList.keys_mk

added theorem AList.mem_mk

Modified Mathlib/Data/Sigma/Basic.lean

added theorem Prod.toSigma_inj

added theorem Prod.toSigma_injective

Modified Mathlib/SetTheory/Ordinal/CantorNormalForm.lean

added def Ordinal.CNF.coeff

added theorem Ordinal.CNF.coeff_of_le_one

added theorem Ordinal.CNF.coeff_of_mem_CNF

added theorem Ordinal.CNF.coeff_of_not_mem_CNF

added theorem Ordinal.CNF.coeff_one_left

added theorem Ordinal.CNF.coeff_zero_apply

added theorem Ordinal.CNF.coeff_zero_left

added theorem Ordinal.CNF.coeff_zero_right