Skip to content

[Merged by Bors] - feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)#28179

Closed
vihdzp wants to merge 41 commits intoleanprover-community:masterfrom
vihdzp:vi.arch_mul
Closed

[Merged by Bors] - feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)#28179
vihdzp wants to merge 41 commits intoleanprover-community:masterfrom
vihdzp:vi.arch_mul

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Aug 10, 2025 •
edited
Loading

We define addition on ArchimedeanClass R such that mk (a * b) = mk a + mk b, as well as a zero element 0 = mk 1. This makes ArchimedeanClass R into a LinearOrderedAddCommMonoidWithTop when R is a ring, and a LinearOrderedAddCommGroupWithTop when R is a field.

See Zulip for discussion on this (in particular, why we turn multiplication into addition).

Open in Gitpod

@vihdzp vihdzp requested a review from wwylele August 10, 2025 11:02
@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Aug 10, 2025
@github-actions
Copy link
Copy Markdown

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

PR summary 4c2ba0710b

Import changes for modified files

No significant changes to the import graph

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

Declarations diff

+ addValuation
+ addValuation_apply
+ add_left_cancel_of_ne_top
+ add_right_cancel_of_ne_top
+ instance : Add (ArchimedeanClass R)
+ instance : AddCommMagma (ArchimedeanClass R)
+ instance : AddCommMonoid (ArchimedeanClass R)
+ instance : IsOrderedAddMonoid (ArchimedeanClass R)
+ instance : LinearOrderedAddCommGroupWithTop (ArchimedeanClass R)
+ instance : LinearOrderedAddCommMonoidWithTop (ArchimedeanClass R)
+ instance : Neg (ArchimedeanClass R)
+ instance : SMul ℕ (ArchimedeanClass R)
+ instance : SMul ℤ (ArchimedeanClass R)
+ instance : Zero (ArchimedeanClass R)
+ lift₂
+ lift₂_mk
+ mk_inv
+ mk_mul
+ mk_one
+ mk_pow
+ mk_zpow
+ top_eq_mk_iff

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

@vihdzp vihdzp changed the title feat: Add (ArchimedeanClass M) feat: LinearOrderedAddCommMonoidWithTop (ArchimedeanClass M) Aug 10, 2025
@vihdzp vihdzp marked this pull request as draft August 10, 2025 12:02
@vihdzp vihdzp changed the title feat: LinearOrderedAddCommMonoidWithTop (ArchimedeanClass M) feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass M) Aug 10, 2025
@vihdzp vihdzp marked this pull request as ready for review August 10, 2025 12:48
wwylele
wwylele reviewed Aug 10, 2025
View reviewed changes
wwylele
wwylele reviewed Aug 10, 2025
View reviewed changes
Copy link
Copy Markdown
Collaborator

@wwylele wwylele left a comment

Choose a reason for hiding this comment

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

Looks mostly good. Thanks!

@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 Aug 14, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Aug 14, 2025

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

alreadydone
alreadydone reviewed Aug 15, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

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

Can you merge master please?

@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 Aug 15, 2025
alreadydone
alreadydone reviewed Aug 16, 2025
View reviewed changes
@vihdzp vihdzp changed the title feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass M) feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) Aug 16, 2025
@alreadydone
Copy link
Copy Markdown
Contributor

alreadydone commented Aug 17, 2025

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 17, 2025

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 17, 2025
@wwylele wwylele mentioned this pull request Aug 17, 2025
Closed
@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
@vihdzp @wwylele @alreadydone
feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) (#28179)
df7889c 
We define addition on `ArchimedeanClass R` such that `mk (a * b) = mk a + mk b`, as well as a zero element `0 = mk 1`. This makes `ArchimedeanClass R` into a `LinearOrderedAddCommMonoidWithTop` when `R` is a ring, and a `LinearOrderedAddCommGroupWithTop` when `R` is a field.

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@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: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) [Merged by Bors] - feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) Sep 1, 2025
@mathlib-bors mathlib-bors bot closed this Sep 1, 2025
CBirkbeck pushed a commit to CBirkbeck/mathlib4 that referenced this pull request Sep 8, 2025
@vihdzp @wwylele
@alreadydone @CBirkbeck
feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) (leanpr…
f6cdc04 
…over-community#28179)

We define addition on `ArchimedeanClass R` such that `mk (a * b) = mk a + mk b`, as well as a zero element `0 = mk 1`. This makes `ArchimedeanClass R` into a `LinearOrderedAddCommMonoidWithTop` when `R` is a ring, and a `LinearOrderedAddCommGroupWithTop` when `R` is a field.

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
yuanyi-350 pushed a commit to yuanyi-350/yuanyi_mathlib4 that referenced this pull request Sep 10, 2025
@vihdzp @wwylele
@alreadydone @yuanyi-350
feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) (leanpr…
29a30d8 
…over-community#28179)

We define addition on `ArchimedeanClass R` such that `mk (a * b) = mk a + mk b`, as well as a zero element `0 = mk 1`. This makes `ArchimedeanClass R` into a `LinearOrderedAddCommMonoidWithTop` when `R` is a ring, and a `LinearOrderedAddCommGroupWithTop` when `R` is a field.

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@vihdzp @wwylele
@alreadydone @joelriou
feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) (leanpr…
e4a8a62 
…over-community#28179)

We define addition on `ArchimedeanClass R` such that `mk (a * b) = mk a + mk b`, as well as a zero element `0 = mk 1`. This makes `ArchimedeanClass R` into a `LinearOrderedAddCommMonoidWithTop` when `R` is a ring, and a `LinearOrderedAddCommGroupWithTop` when `R` is a field.

Co-authored-by: Weiyi Wang <wwylele@gmail.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@vihdzp vihdzp deleted the vi.arch_mul branch March 14, 2026 01:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@alreadydone alreadydone alreadydone approved these changes

+1 more reviewer

@wwylele wwylele wwylele approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@riccardobrasca riccardobrasca

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.

7 participants

@vihdzp @kckennylau @wwylele @mathlib4-merge-conflict-bot @mathlib4-dependent-issues-bot @alreadydone @riccardobrasca