-
Notifications
You must be signed in to change notification settings - Fork 299
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(algebra/ordered_monoid): linear_ordered_add_comm_monoid(_with_top) #6520
Conversation
It would be good to get #6489 merged before this one, so that this PR can include transferring instances of this new class to submonoids. |
…a}): pullback of ordered algebraic structures under an injective map
@awainverse are you ok with waiting for that PR? I expect that it moves on the merge queue in the next two hours. |
I don't mind waiting. If I'm too impatient I'll just throw up an |
Alright, #6489 is on the queue. Could you also add in this PR:
You should be able to copy the approach verbatim from the versions without |
…stances' into linear_ordered_comm_monoid
Ok, this now genuinely depends on #6489, I've added those lemmas. |
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
bors d=@eric-wieser |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks! Just CI to wait on bors d=@awainverse |
✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…p) (#6520) Separates out classes for `linear_ordered_(add_)comm_monoid` Creates `linear_ordered_add_comm_monoid_with_top`, an additive and order-reversed version of `linear_ordered_comm_monoid_with_zero`. Puts an instance of `linear_ordered_add_comm_monoid_with_top` on `with_top` of any `linear_ordered_add_comm_monoid` and also on `enat` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…p) (#6520) Separates out classes for `linear_ordered_(add_)comm_monoid` Creates `linear_ordered_add_comm_monoid_with_top`, an additive and order-reversed version of `linear_ordered_comm_monoid_with_zero`. Puts an instance of `linear_ordered_add_comm_monoid_with_top` on `with_top` of any `linear_ordered_add_comm_monoid` and also on `enat` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Separates out classes for
linear_ordered_(add_)comm_monoid
Creates
linear_ordered_add_comm_monoid_with_top
, an additive and order-reversed version oflinear_ordered_comm_monoid_with_zero
.Puts an instance of
linear_ordered_add_comm_monoid_with_top
onwith_top
of anylinear_ordered_add_comm_monoid
and also onenat
The goal is additive valuations - see https://github.com/leanprover-community/mathlib/tree/add_valuation3