mathlib3

4b9f0482 - feat(set_theory/principal): Define `principal` ordinals (#11679)

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.