mathlib3
196a48c8 - feat(set_theory/ordinal_arithmetic): Coefficients of Cantor Normal Form (#12681)

Commit
3 years ago
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.
Author
Parents
Loading