Skip to content

[Merged by Bors] - feat: Hahn embedding theorem#27268

Closed
wwylele wants to merge 2 commits intoleanprover-community:masterfrom
wwylele:wwylele-hahn
Closed

[Merged by Bors] - feat: Hahn embedding theorem#27268
wwylele wants to merge 2 commits intoleanprover-community:masterfrom
wwylele:wwylele-hahn

Conversation

@wwylele
Copy link
Copy Markdown
Collaborator

@wwylele wwylele commented Jul 18, 2025 •
edited
Loading

This proves Hahn embedding theorem, one among the 1000+ theorems project.

Note on file location: I originally placed it in Algebra/Order/Group, but got prompted that Algebra can't import Analysis (needed for Real being a Rat-module` and related fact), so now I moved it under HahnSeries

This is migrated from #25140 to fork

Open in Gitpod

@wwylele wwylele mentioned this pull request Jul 18, 2025
Closed
7 tasks
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jul 18, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 18, 2025 •
edited
Loading

PR summary e11b36c7ea

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.HahnSeries.HahnEmbedding (new file) 1624

Declarations diff

+ hahnEmbedding_isOrderedAddMonoid
+ hahnEmbedding_isOrderedModule_rat
+ instance : Nonempty (HahnEmbedding.Seed ℚ M ℝ) := by

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 18, 2025
@wwylele wwylele force-pushed the wwylele-hahn branch 3 times, most recently from 0326930 to 13db80f Compare July 19, 2025 03:09
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 19, 2025

This pull request has conflicts, please merge master and resolve them.

@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 Jul 19, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 25, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 27, 2025

This pull request has conflicts, please merge master and resolve them.

@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 Jul 27, 2025
@wwylele wwylele mentioned this pull request Jul 27, 2025
Closed
@grunweg grunweg added the t-algebra Algebra (groups, rings, fields, etc) label Aug 4, 2025
@wwylele wwylele mentioned this pull request Sep 3, 2025
Closed
3 tasks
@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Sep 7, 2025
This was referenced Sep 8, 2025
Closed
Closed
wwylele added a commit to wwylele/mathlib4 that referenced this pull request Sep 8, 2025
@wwylele
feat(Algebra/Order): ArchimedeanClass.ball ≤ .closedBall
5b5d693 
One missing lemma that will be used in leanprover-community#27268 Hahn embedding theorem
wwylele added a commit to wwylele/mathlib4 that referenced this pull request Sep 8, 2025
@wwylele
feat(RingTheory/HahnSeries): embDomain as OrderAddMonoidHom; orderTop…
4cebe04 
… of embDomain

These will be used in leanprover-community#27268 Hahn embedding theorem
wwylele added a commit to wwylele/mathlib4 that referenced this pull request Sep 8, 2025
@wwylele
feat(RingTheory/HahnSeries): embDomain as OrderAddMonoidHom; orderTop…
1ff1645 
… of embDomain

These will be used in leanprover-community#27268 Hahn embedding theorem
wwylele added a commit to wwylele/mathlib4 that referenced this pull request Sep 8, 2025
@wwylele
feat(Algebra/Order): ArchimedeanClass.ball ≤ .closedBall
d7a8802 
One missing lemma that will be used in leanprover-community#27268 Hahn embedding theorem
@wwylele wwylele mentioned this pull request Sep 8, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Sep 9, 2025
@wwylele
feat(Algebra/Order): OrderIso on FiniteArchimedeanClass from OrderIso…
4a587d4 
… on all classes (#29451)

This will be used in #27268 Hahn embedding theorem
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot 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 9, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Sep 9, 2025

This pull request has conflicts, please merge master and resolve them.

mathlib-bors bot pushed a commit that referenced this pull request Oct 9, 2025
@wwylele
feat(GroupTheory): add DivisibleHull (#29275)
6a1dc6b 
This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.
@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Oct 9, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 9, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Oct 9, 2025

This PR/issue depends on:

@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Oct 9, 2025

This last part is now ready for review!

@wwylele wwylele assigned YaelDillies and unassigned YaelDillies Oct 10, 2025
@wwylele wwylele requested a review from YaelDillies October 10, 2025 14:32
YaelDillies
YaelDillies approved these changes Oct 10, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks! That's a great milestone!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 10, 2025

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 10, 2025
@wwylele @YaelDillies
Update Mathlib/RingTheory/HahnSeries/HahnEmbedding.lean
faee0b2 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Oct 11, 2025

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 11, 2025

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Oct 11, 2025
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Oct 11, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Oct 11, 2025
@wwylele
feat: Hahn embedding theorem (#27268)
3da7809 
This proves [Hahn embedding theorem](https://en.wikipedia.org/wiki/Hahn_embedding_theorem), one among the 1000+ theorems project.

Note on file location: I originally placed it in Algebra/Order/Group, but got prompted that Algebra can't import Analysis (needed for `Real` being a `Rat`-module` and related fact), so now I moved it under HahnSeries
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 11, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Hahn embedding theorem [Merged by Bors] - feat: Hahn embedding theorem Oct 11, 2025
@mathlib-bors mathlib-bors bot closed this Oct 11, 2025
@wwylele wwylele deleted the wwylele-hahn branch October 11, 2025 15:33
Jlh18 pushed a commit to Jlh18/mathlib4 that referenced this pull request Oct 14, 2025
@wwylele @Jlh18
feat(Algebra/HahnEmbedding): ArchimedeanStrata is non-empty (leanprov…
e2b1225 
…er-community#30101)

This is a small part of leanprover-community#27268 (Hahn embedding theorem). Separated out for easy review while waiting for the other dependency.
Jlh18 pushed a commit to Jlh18/mathlib4 that referenced this pull request Oct 14, 2025
@wwylele @Jlh18
feat(GroupTheory): add DivisibleHull (leanprover-community#29275)
8eb30c3 
This is part of Hahn embedding theorem leanprover-community#27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at leanprover-community#25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@wwylele @BeibeiX0
feat(Algebra/HahnEmbedding): ArchimedeanStrata is non-empty (leanprov…
d477d70 
…er-community#30101)

This is a small part of leanprover-community#27268 (Hahn embedding theorem). Separated out for easy review while waiting for the other dependency.
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@wwylele @BeibeiX0
feat(GroupTheory): add DivisibleHull (leanprover-community#29275)
59ab80b 
This is part of Hahn embedding theorem leanprover-community#27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at leanprover-community#25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@wwylele @BeibeiX0
feat: Hahn embedding theorem (leanprover-community#27268)
80bca59 
This proves [Hahn embedding theorem](https://en.wikipedia.org/wiki/Hahn_embedding_theorem), one among the 1000+ theorems project.

Note on file location: I originally placed it in Algebra/Order/Group, but got prompted that Algebra can't import Analysis (needed for `Real` being a `Rat`-module` and related fact), so now I moved it under HahnSeries
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@wwylele @leanprover-community-bot-assistant @mathlib4-merge-conflict-bot @mathlib4-dependent-issues-bot @riccardobrasca @YaelDillies @grunweg