Skip to content

[Merged by Bors] - feat(Algebra/Order): ArchimedeanClass ball for module#28449

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

[Merged by Bors] - feat(Algebra/Order): ArchimedeanClass ball for module#28449
wwylele wants to merge 3 commits intoleanprover-community:masterfrom
wwylele:wwylele-hahn-ball2

Conversation

@wwylele
Copy link
Copy Markdown
Collaborator

@wwylele wwylele commented Aug 14, 2025

This continues #27885 and promotes ArchimedeanClass.addSubgroup to a submodule. Balls are promoted to submodules with shorter names ball and closedBall, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to ballSubmodule and closedBallSubmodule)

Open in Gitpod

@wwylele wwylele mentioned this pull request Aug 14, 2025
Closed
7 tasks
@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Aug 14, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 14, 2025 •
edited
Loading

PR summary 5275857c30

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Order.Module.Archimedean (new file) 836

Declarations diff

+ ball
+ ball_antitone
+ ball_top
+ closedBall
+ closedBall_top
+ mem_ball_iff
+ mem_closedBall_iff
+ mk_le_mk_smul
+ mk_smul
+ submodule
+ toAddSubgroup_ball
+ toAddSubgroup_closedBall

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).

@wwylele wwylele requested a review from YaelDillies August 15, 2025 00:48
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Aug 17, 2025 •
edited
Loading

Extracted the smul lemma and sharpened it a little bit

I also tried generalize it from Module to weaker SMul instances, but it didn't quite work. The current form basically needs distributive neg. The lemma likely also works with canonically ordered semirings, but it will take a different form so I left it out

@wwylele wwylele force-pushed the wwylele-hahn-ball2 branch from 4731303 to 6e5e86f Compare August 17, 2025 17:10
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Aug 17, 2025

Another note: when #28179 is merged, result here can be generalized to non-archimedean scalars, in which case one can define mk (k • a) = mk k +ᵥ mk a (mk k already belongs to an AddCommGroup). This doesn't help my project and feels over-engineered at the moment, so I don't plan to implement it any time soon.

@wwylele wwylele force-pushed the wwylele-hahn-ball2 branch from 6e5e86f to 3f1b171 Compare August 28, 2025 22:44
@YaelDillies YaelDillies assigned YaelDillies and unassigned kim-em Aug 29, 2025
YaelDillies
YaelDillies approved these changes Aug 29, 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!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 29, 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 Aug 29, 2025
@wwylele @YaelDillies
Update Mathlib/Algebra/Order/Module/Archimedean.lean
e23aba7 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Sep 1, 2025

Thanks!

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Sep 1, 2025
mathlib-bors bot pushed a commit that referenced this pull request Sep 1, 2025
@wwylele
feat(Algebra/Order): ArchimedeanClass ball for module (#28449)
f21b9bf 
This continues #27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 1, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Sep 1, 2025
@wwylele
feat(Algebra/Order): ArchimedeanClass ball for module (#28449)
ee46555 
This continues #27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 1, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Sep 1, 2025
@wwylele
feat(Algebra/Order): ArchimedeanClass ball for module (#28449)
88a075c 
This continues #27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 1, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Order): ArchimedeanClass ball for module [Merged by Bors] - feat(Algebra/Order): ArchimedeanClass ball for module Sep 1, 2025
@mathlib-bors mathlib-bors bot closed this Sep 1, 2025
@wwylele wwylele deleted the wwylele-hahn-ball2 branch September 2, 2025 01:31
CBirkbeck pushed a commit to CBirkbeck/mathlib4 that referenced this pull request Sep 8, 2025
@wwylele @CBirkbeck
feat(Algebra/Order): ArchimedeanClass ball for module (leanprover-com…
4982239 
…munity#28449)

This continues leanprover-community#27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)
yuanyi-350 pushed a commit to yuanyi-350/yuanyi_mathlib4 that referenced this pull request Sep 10, 2025
@wwylele @yuanyi-350
feat(Algebra/Order): ArchimedeanClass ball for module (leanprover-com…
cf2a54f 
…munity#28449)

This continues leanprover-community#27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@wwylele @joelriou
feat(Algebra/Order): ArchimedeanClass ball for module (leanprover-com…
a81f526 
…munity#28449)

This continues leanprover-community#27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)
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

@YaelDillies YaelDillies

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@wwylele @riccardobrasca @YaelDillies @kim-em