Commit 2022-04-01 19:21 196a48c8

View on Github →

feat(set_theory/ordinal_arithmetic): Coefficients of Cantor Normal Form (#12681) We prove all coefficients of the base-b expansion of an ordinal are less than b. We also tweak the parameters of various other theorems.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

modified def ordinal.CNF

modified theorem ordinal.CNF_fst_le

modified theorem ordinal.CNF_fst_le_log

added theorem ordinal.CNF_lt_snd

modified theorem ordinal.CNF_pairwise

modified theorem ordinal.CNF_snd_lt

modified theorem ordinal.CNF_sorted

modified theorem ordinal.one_CNF