Skip to content

[Merged by Bors] - feat(Topology/ValuativeRel): helper instance for Valued from ValuativeTopology#26713

Closed
pechersky wants to merge 5 commits intoleanprover-community:masterfrom
pechersky:valuative-top-valued
Closed

[Merged by Bors] - feat(Topology/ValuativeRel): helper instance for Valued from ValuativeTopology#26713
pechersky wants to merge 5 commits intoleanprover-community:masterfrom
pechersky:valuative-top-valued

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Jul 4, 2025 •
edited
Loading

pechersky added 2 commits July 3, 2025 17:43
@pechersky
feat(RingTheory/ValuativeRel): additional API to prepare for refactor
d69e17a 
some helper lemmas that will be used in downstream refactor of Valued PRs
@pechersky
feat(Topology/ValuativeRel): helper instance for Valued from Valuativ…
12034fa 
…eTopology

and lemmas on clopen balls
@github-actions
Copy link
Copy Markdown

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

PR summary 00c9085f64

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Topology.Algebra.Valued.ValuativeRel (new file) 1421

Declarations diff

+ hasBasis_nhds_zero
+ instance [UniformSpace R] [IsUniformAddGroup R] [ValuativeRel R] [ValuativeTopology R] :
+ isClopen_ball
+ isClopen_closedBall
+ isClopen_sphere
+ isClosed_ball
+ isClosed_closedBall
+ isOpen_ball
+ isOpen_closedBall
+ isOpen_sphere
+ mem_nhds

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 4, 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 Jul 5, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jul 5, 2025

This PR/issue depends on:

@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 5, 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 5, 2025
@pechersky pechersky mentioned this pull request Jul 6, 2025
Open
2 tasks
@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 6, 2025
@pechersky pechersky added t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-analysis Analysis (normed *, calculus) t-algebra Algebra (groups, rings, fields, etc) labels Jul 6, 2025
This was referenced Jul 7, 2025
Closed
Closed
kbuzzard
kbuzzard reviewed Jul 7, 2025
View reviewed changes
kbuzzard
kbuzzard reviewed Jul 7, 2025
View reviewed changes
kbuzzard
kbuzzard reviewed Jul 7, 2025
View reviewed changes
kbuzzard
kbuzzard reviewed Jul 7, 2025
View reviewed changes
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jul 7, 2025

LGTM. Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 7, 2025

✌️ pechersky 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 the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 7, 2025
@pechersky
Copy link
Copy Markdown
Contributor Author

pechersky commented Jul 7, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jul 7, 2025
@pechersky
feat(Topology/ValuativeRel): helper instance for Valued from Valuativ…
f2f4294 
…eTopology (#26713)

and lemmas on clopen balls



Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology/ValuativeRel): helper instance for Valued from ValuativeTopology [Merged by Bors] - feat(Topology/ValuativeRel): helper instance for Valued from ValuativeTopology Jul 7, 2025
@mathlib-bors mathlib-bors bot closed this Jul 7, 2025
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Jul 16, 2025
@pechersky @BeibeiX0
feat(Topology/ValuativeRel): helper instance for Valued from Valuativ…
8a523aa 
…eTopology (leanprover-community#26713)

and lemmas on clopen balls



Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@pechersky @callesonne
feat(Topology/ValuativeRel): helper instance for Valued from Valuativ…
0ff9514 
…eTopology (leanprover-community#26713)

and lemmas on clopen balls



Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@pechersky @hrmacbeth
feat(Topology/ValuativeRel): helper instance for Valued from Valuativ…
aa2279d 
…eTopology (leanprover-community#26713)

and lemmas on clopen balls



Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kbuzzard kbuzzard kbuzzard left review comments

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) t-analysis Analysis (normed *, calculus) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@pechersky @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @kbuzzard