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(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API #14656
Conversation
…munity/mathlib into valuation_maximal
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.
I'm happy with this but wrote part of it, could someone else do another check?
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
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.
LGTM!
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.
Thanks 🎉
bors merge
…of valuation subring and provide basic API (#14656) This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: jackmckoen <104791831+jackmckoen@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…of valuation subring and provide basic API (leanprover-community#14656) This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: jackmckoen <104791831+jackmckoen@users.noreply.github.com>
…of valuation subring and provide basic API (#14656) This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: jackmckoen <104791831+jackmckoen@users.noreply.github.com>
…of valuation subring and provide basic API (#14656) This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: jackmckoen <104791831+jackmckoen@users.noreply.github.com>
This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal.