Commit 2022-02-01 02:13 4b9f0482

feat(set_theory/principal): Define principal ordinals (#11679) An ordinal o is said to be principal or indecomposable under an operation when the set of ordinals less than it is closed under that operation. In standard mathematical usage, this term is almost exclusively used for additive and multiplicative principal ordinals. For simplicity, we break usual convention and regard 0 as principal.