-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(set_theory/principal): prove theorems about additive principal ordinals #11704
Conversation
…s evaluated at `ω` Somewhat branched off of #11270
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks very clean to me, I have no substantial comments!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
covariant_class
instances for ordinal addition and multiplication #11678principal
ordinals #11679Split off from #11701. I'm really sorry, I truly don't mean to spam PRs. If all goes well I'll repurpose that PR for multiplicative principals.
Splitting off only the theorems on additive principal ordinals leaves
ordinal_arithmetic
in a really awkward state, where it doesn't contain theorems on additive principals yet contains various theorems on multiplicative and exponential principals, stated differently. Fortunately these theorems aren't really used much inmathlib
, so this temporary awkwardness isn't too much of a problem.Splitting off the multiplicative principal results and adding everything else of relevance would make the PR huge. Trust me, I've tried.