[Merged by Bors] - feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot by xgenereux · Pull Request #33631 · leanprover-community/mathlib4

xgenereux · 2026-01-05T22:12:04Z

simp lemmas for idealOfLE/ofPrime in the trivial cases of ⊥, ⊤ .

This is my second try at this PR (after I bailed on #33618), sorry about this!

Co-authored-by: María Inés de Frutos Fernández <[email protected]>

depends on: [Merged by Bors] - feat(ValuationSubring): fieldTop #33612
depends on: [Merged by Bors] - refactor: Ideal.bot_prime as an instance #33609

github-actions · 2026-01-05T22:13:06Z

PR summary 808d25cae3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ idealOfLE_self
+ idealOfLE_top
+ inclusion_injective
+ ofPrime_bot
+ ofPrime_top

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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-merge-conflict-bot · 2026-01-13T21:29:27Z

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

mathlib4-merge-conflict-bot · 2026-01-21T08:37:49Z

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

mathlib4-dependent-issues-bot · 2026-01-21T08:44:44Z

This PR/issue depends on:

~~[Merged by Bors] - feat(ValuationSubring): fieldTop #33612~~
~~[Merged by Bors] - refactor: Ideal.bot_prime as an instance #33609~~
By Dependent Issues (🤖). Happy coding!

Mathlib/RingTheory/Valuation/ValuationSubring.lean

Vierkantor

Looks good to me otherwise! 🎉

bors d+

mathlib-bors · 2026-03-09T12:06:31Z

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

Mathlib/RingTheory/Valuation/ValuationSubring.lean

xgenereux · 2026-03-16T16:31:10Z

bors r+

… to top/bot (#33631) simp lemmas for `idealOfLE`/`ofPrime` in the trivial cases of `⊥`, `⊤` . This is my second try at this PR (after I bailed on #33618), sorry about this! Co-authored-by: María Inés de Frutos Fernández <[[email protected]](mailto:[email protected])> Co-authored-by: Xavier Genereux <[email protected]>

mathlib-bors · 2026-03-16T17:41:26Z

Build failed (retrying...):

ci (staging) / Build

… to top/bot (#33631) simp lemmas for `idealOfLE`/`ofPrime` in the trivial cases of `⊥`, `⊤` . This is my second try at this PR (after I bailed on #33618), sorry about this! Co-authored-by: María Inés de Frutos Fernández <[[email protected]](mailto:[email protected])> Co-authored-by: Xavier Genereux <[email protected]>

mathlib-bors · 2026-03-16T18:35:01Z

Build failed (retrying...):

ci (staging) / Build

… to top/bot (#33631) simp lemmas for `idealOfLE`/`ofPrime` in the trivial cases of `⊥`, `⊤` . This is my second try at this PR (after I bailed on #33618), sorry about this! Co-authored-by: María Inés de Frutos Fernández <[[email protected]](mailto:[email protected])> Co-authored-by: Xavier Genereux <[email protected]>

mathlib-bors · 2026-03-16T19:06:45Z

Pull request successfully merged into master.

Build succeeded:

xgenereux added 8 commits January 5, 2026 17:06

feat(ValuationSubring): fieldTop

cd9a209

add docstring

b25319c

golf

e2be181

refactor: Ideal.bot_prime as an instance

576f539

rename + remove have := bot_prime

1318c2d

fix error

09b65ff

suggested rename

23b2416

feat(ValuationSubring): idealOfLE/ofPrime_bot/top

f80a6c2

xgenereux mentioned this pull request Jan 5, 2026

[Merged by Bors] - feat(ValuationSubring): eq_self_or_eq_top_of_le #33634

Closed

4 tasks

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 Jan 5, 2026

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 Jan 13, 2026

update mathlib

68f634d

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 Jan 13, 2026

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 Jan 21, 2026

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 Jan 21, 2026

joneugster added the t-algebra Algebra (groups, rings, fields, etc) label Feb 1, 2026

update Mathlib

c3dabda

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 Feb 7, 2026

remove depr. call

1d3bcce

mathlib-triage bot assigned alreadydone Feb 11, 2026

xgenereux assigned erdOne Mar 1, 2026

xgenereux mentioned this pull request Mar 6, 2026

feat: localizations of primes in Dedekind domains are valuation subrings #33010

Open

2 tasks

update mathlib

64dd0cf

Vierkantor self-requested a review March 9, 2026 11:54

Vierkantor reviewed Mar 9, 2026

View reviewed changes

Mathlib/RingTheory/Valuation/ValuationSubring.lean Outdated Show resolved Hide resolved

Vierkantor approved these changes Mar 9, 2026

View reviewed changes

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 9, 2026

suggested changes

a737a76

faenuccio reviewed Mar 11, 2026

View reviewed changes

Mathlib/RingTheory/Valuation/ValuationSubring.lean Outdated Show resolved Hide resolved

faenuccio reviewed Mar 11, 2026

View reviewed changes

Mathlib/RingTheory/Valuation/ValuationSubring.lean Outdated Show resolved Hide resolved

faenuccio reviewed Mar 11, 2026

View reviewed changes

Mathlib/RingTheory/Valuation/ValuationSubring.lean Show resolved Hide resolved

xgenereux added 4 commits March 16, 2026 10:52

suggested changes

a07b246

remove simp tag

2b439d3

remove unnec. simp arg

0e3943b

remove parenth

2cec632

mathlib-bors bot changed the title ~~feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot~~ [Merged by Bors] - feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot Mar 16, 2026

mathlib-bors bot closed this Mar 16, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot#33631

[Merged by Bors] - feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot#33631
xgenereux wants to merge 17 commits intoleanprover-community:masterfrom
xgenereux:idealOfLE-ofPrime_bot-top

xgenereux commented Jan 5, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Jan 5, 2026 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Jan 13, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Jan 21, 2026

Uh oh!

mathlib4-dependent-issues-bot commented Jan 21, 2026

Uh oh!

Uh oh!

Vierkantor left a comment

Uh oh!

mathlib-bors bot commented Mar 9, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

xgenereux commented Mar 16, 2026

Uh oh!

mathlib-bors bot commented Mar 16, 2026

Uh oh!

mathlib-bors bot commented Mar 16, 2026

Uh oh!

mathlib-bors bot commented Mar 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

Conversation

xgenereux commented Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 808d25cae3

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Jan 13, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Jan 21, 2026

Uh oh!

mathlib4-dependent-issues-bot commented Jan 21, 2026

Uh oh!

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 9, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

xgenereux commented Mar 16, 2026

Uh oh!

mathlib-bors bot commented Mar 16, 2026

Uh oh!

mathlib-bors bot commented Mar 16, 2026

Uh oh!

mathlib-bors bot commented Mar 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

xgenereux commented Jan 5, 2026 •

edited

Loading

github-actions bot commented Jan 5, 2026 •

edited

Loading