Commit 2024-10-16 11:05 fde83d96
View on Github →feat(SetTheory/Ordinal/Principal): simpler characterization of Principal for monotone operations (#17742)
plus some drive-by spacing fixes.
Subsequent PRs will use this to golf results on additive and multiplicative principal ordinals.