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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(ring_theory/valuation/valuation_subring): define principal unit group of valuation subring and provide basic API #14742

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat(ring_theory/valuation/valuation_subring): define principal unit group of valuation subring and provide basic API #14742

wants to merge 28 commits into from

Conversation

mckoen
Copy link
Collaborator

@mckoen mckoen commented Jun 14, 2022 •
edited

This PR defines the principal unit group of a valuation subring as a subgroup of the units of the field. We show two valuation subrings are equal iff their principal unit groups are the same, and we show that the map on valuation subrings to their principal unit groups is an order embedding.

Open in Gitpod

@mckoen mckoen added awaiting-author A reviewer has asked the author a question or requested changes blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 14, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 15, 2022
@mckoen mckoen added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 25, 2022
@mckoen mckoen added awaiting-review The author would like community review of the PR awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-author A reviewer has asked the author a question or requested changes awaiting-review The author would like community review of the PR labels Jul 12, 2022
@mckoen mckoen added WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 25, 2022
@mckoen mckoen added the awaiting-review The author would like community review of the PR label Jul 27, 2022
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 29, 2022
@mckoen mckoen added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 29, 2022
@mckoen mckoen added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 2, 2022
@mckoen mckoen added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 8, 2022
@adamtopaz adamtopaz added the t-algebra Algebra (groups, rings, fields etc) label Aug 10, 2022
jcommelin
jcommelin approved these changes Aug 10, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 10, 2022
bors bot pushed a commit that referenced this pull request Aug 10, 2022
@mckoen @adamtopaz
feat(ring_theory/valuation/valuation_subring): define principal unit …
e63df39 
…group of valuation subring and provide basic API (#14742)


This PR defines the principal unit group of a valuation subring as a subgroup of the units of the field. We show two valuation subrings are equal iff their principal unit groups are the same, and we show that the map on valuation subrings to their principal unit groups is an order embedding.



Co-authored-by: Adam Topaz <github@adamtopaz.com>
@bors
Copy link

bors bot commented Aug 10, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/valuation/valuation_subring): define principal unit group of valuation subring and provide basic API [Merged by Bors] - feat(ring_theory/valuation/valuation_subring): define principal unit group of valuation subring and provide basic API Aug 10, 2022
@bors bors bot closed this Aug 10, 2022
@bors bors bot deleted the valuation_principal_units branch August 10, 2022 17:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@adamtopaz adamtopaz adamtopaz left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@mckoen @mathlib-dependent-issues-bot @adamtopaz @jcommelin @leanprover-community-bot-assistant