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

feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered #16619

Open
wants to merge 115 commits into
base: master
Choose a base branch
from
Open

feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered #16619

wants to merge 115 commits into from
+255 −22

Conversation

pechersky
Copy link
Collaborator

@pechersky pechersky commented Sep 9, 2024 •
edited
Loading

pechersky and others added 30 commits August 7, 2024 10:03
@pechersky
feat(Algebra/Order/Archimedean): multiplicativize Archimedean
dbba7e9 
This allows one to talk about finding powers greater than some element for ordered monoids
Before, this was only available for ordered semirings
This is to later installthe instance on valuation groups (`LinearOrderedCommGroupWithZero`)
Install the instance on NNRat and NNReal (though they are ordered semirings)
Also, add some misisng instances about the nonnegative submonoid
@pechersky
feat(GroupTheory/Archimedean): `LinearOrderedAddCommGroup.discrete_or…
b1e8032 
…_denselyOrdered`

Classfy linearly ordered additive groups, either they are discrete (order isomorphic to Int) or densely ordered
Also add some simple lemmas about the closure subgroup.
@pechersky
Merge branch 'master' into pechersky/mul-archimedean
4ab710a
@pechersky
left arrow
0e57f15
@pechersky
unsimp, due to pointwise
e039680
@pechersky
generalize closure equiv
12d7a39
@pechersky
add additive docstring
ca18efa
@pechersky
Merge branch 'pechersky/mul-archimedean' into pechersky/multiplicativ…
a6c4566 
…ize-group-archimedean
@pechersky
feat(GroupTheory/Archimedean): multiplicativize
d325a7b
@pechersky
Merge branch 'pechersky/discrete-or-denselyOrdered' into pechersky/mu…
363ee74 
…ltiplicativize-group-archimedean
@pechersky
feat(GroupTheory/Archimedean): `LinearOrderedCommGroupWithZero.discre…
e733f83 
…te_or_denselyOrdered`

Along with helper equivs about `Units`
and some missing instances about `Units`.
@pechersky
feat(RingTheory): `Valuation.Integers.not_denselyOrdered_of_isPrincip…
591fe49 
…alIdealRing`
@pechersky
feat(Order/SuccPred/TypeTags): SuccOrder (Multiplicative X) and fri…
038d2d9 
…ends
@pechersky
Mathlib.lean
7117da4
@pechersky
feat(Order/SuccPred): BddAbove.exists_isGreatest_of_nonempty
eb3c183 
when `IsSuccArchimedean`
@pechersky
feat(Order/SuccPred): transfer SuccOrder, IsSuccArchimedean
679a75b 
across monotone equivs
@pechersky
docstrings
705807c
@pechersky
reduce line count
55a03e9
@pechersky
feedback
526e85e
@pechersky
feedback
a001674
@pechersky
feat(Algebra/Order/Hom): Order(Add)MonoidIso
07a7465
@pechersky
bring instance back
b049050
@pechersky
move to pointwise
e5b8fcb
@pechersky
change import
f869164
@pechersky
fix naming
876152d
@pechersky
Merge branch 'master' into pechersky/bddabove-exists-is-greatest-succ…
5dd72ee 
…arch
@pechersky
linear order now necessary
7642ea1
@pechersky
Merge branch 'master' into pechersky/succ-order-type-tags
dff4d8c
@pechersky
Merge branch 'master' into pechersky/succ-order-transfer
d5e0aa4
@pechersky
remove obsolete field
92847b1
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 10, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 12, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 12, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 12, 2024
@pechersky pechersky mentioned this pull request Sep 12, 2024
Open
3 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 16, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 17, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 17, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 17, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 18, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@pechersky @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant