Skip to content

[Merged by Bors] - chore(ContinuousMap/Compact): generalize to seminormed spaces#17526

Closed
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/more-seminormed
Closed

[Merged by Bors] - chore(ContinuousMap/Compact): generalize to seminormed spaces#17526
eric-wieser wants to merge 2 commits intomasterfrom
eric-wieser/more-seminormed

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Oct 7, 2024

Also add a bunch of missing NormedRing-adjacent instances.

Open in Gitpod

@eric-wieser eric-wieser added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Oct 7, 2024
@eric-wieser eric-wieser mentioned this pull request Oct 7, 2024
Closed
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 7, 2024 •
edited
Loading

PR summary 1de4ca3e9e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instMetricSpace
+ instPseudoMetricSpace
+ instance : SeminormedAddCommGroup C(α, E)
+ instance [NonUnitalNormedCommRing R] : NonUnitalNormedCommRing C(α, R)
+ instance [NonUnitalNormedRing R] : NonUnitalNormedRing C(α, R)
+ instance [NonUnitalSeminormedCommRing R] : NonUnitalSeminormedCommRing C(α, R)
+ instance [NonUnitalSeminormedRing R] : NonUnitalSeminormedRing C(α, R)
+ instance [NormedCommRing R] : NormedCommRing C(α, R)
+ instance [NormedRing R] : NormedRing C(α, R)
+ instance [SeminormedCommRing R] : SeminormedCommRing C(α, R)
+ instance [SeminormedRing R] : SeminormedRing C(α, R)
+ instance {E : Type*} [NormedAddCommGroup E] : NormedAddCommGroup C(α, E)
+ instance {R} [Zero R] [Zero β] [PseudoMetricSpace R] [SMul R β] [BoundedSMul R β] :
- instance : NormedAddCommGroup C(α, E)
- instance : NormedRing C(α, R)
- metricSpace

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.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Oct 8, 2024

This looks straightforward to me - I'll be happy to learn about any further implications I'm not yet aware of. (Should this be benchmarked? Is the page up again?)
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 8, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 8, 2024
jcommelin
jcommelin reviewed Oct 8, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 8, 2024
@eric-wieser
chore(ContinuousMap/Compact): generalize to seminormed spaces (#17526)
7740499 
Also add a bunch of missing `NormedRing`-adjacent instances.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(ContinuousMap/Compact): generalize to seminormed spaces [Merged by Bors] - chore(ContinuousMap/Compact): generalize to seminormed spaces Oct 8, 2024
@mathlib-bors mathlib-bors bot closed this Oct 8, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/more-seminormed branch October 8, 2024 10:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@eric-wieser @grunweg @jcommelin