Skip to content
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] - refactor(ring_theory/valuation): valuations in linear_ordered_comm_monoid_with_zero #6500

Closed
wants to merge 2 commits into from

Conversation

awainverse
Copy link
Collaborator

Generalizes the value group in a valuation to a linear_ordered_comm_monoid_with_zero


@awainverse awainverse added the awaiting-review The author would like community review of the PR label Mar 2, 2021
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Assuming most of the lemmas have just moved, this looks fine to me

@awainverse
Copy link
Collaborator Author

I haven't changed anything except the instance assumptions and the organization.

Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a few docstring cleanup suggestions while we're at it. Otherwise LGTM.
bors d+

src/ring_theory/valuation/basic.lean Outdated Show resolved Hide resolved
src/ring_theory/valuation/basic.lean Outdated Show resolved Hide resolved
src/ring_theory/valuation/basic.lean Outdated Show resolved Hide resolved
src/ring_theory/valuation/basic.lean Outdated Show resolved Hide resolved
src/ring_theory/valuation/basic.lean Outdated Show resolved Hide resolved
src/ring_theory/valuation/basic.lean Outdated Show resolved Hide resolved
src/ring_theory/valuation/basic.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Mar 2, 2021

✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@bryangingechen bryangingechen added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Mar 2, 2021
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@awainverse
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Mar 2, 2021
…onoid_with_zero` (#6500)

Generalizes the value group in a `valuation` to a `linear_ordered_comm_monoid_with_zero`



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
@bors
Copy link

bors bot commented Mar 2, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(ring_theory/valuation): valuations in linear_ordered_comm_monoid_with_zero [Merged by Bors] - refactor(ring_theory/valuation): valuations in linear_ordered_comm_monoid_with_zero Mar 2, 2021
@bors bors bot closed this Mar 2, 2021
@bors bors bot deleted the monoid_valuation branch March 2, 2021 23:24
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
…onoid_with_zero` (#6500)

Generalizes the value group in a `valuation` to a `linear_ordered_comm_monoid_with_zero`



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants