Skip to content

[Merged by Bors] - feat(Analysis/Normed/{Group,Field}/Ultra): Nonarchimedean norms from ultrametrics#14768

Closed
pechersky wants to merge 57 commits intomasterfrom
pechersky/ultrametric-space-normed
Closed

[Merged by Bors] - feat(Analysis/Normed/{Group,Field}/Ultra): Nonarchimedean norms from ultrametrics#14768
pechersky wants to merge 57 commits intomasterfrom
pechersky/ultrametric-space-normed

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Jul 15, 2024 •
edited by loefflerd
Loading

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 15, 2024 •
edited
Loading

PR summary 4349689e6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.Normed.Group.Ultra 912
Mathlib.Analysis.Normed.Ring.Ultra 1059

Declarations diff

+ _root_.Finset.Nonempty.norm_prod_le_sup'_norm
+ _root_.Finset.nnnorm_prod_le_sup_nnnorm
+ dist_eq_max_of_dist_ne_dist
+ isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm
+ isUltrametricDist_of_forall_norm_mul_le_max_norm
+ isUltrametricDist_of_isNonarchimedean_nnnorm
+ isUltrametricDist_of_isNonarchimedean_norm
+ nnnorm_add_one_le_max_nnnorm_one
+ nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div
+ nnnorm_eq_of_mul_nnnorm_lt_max
+ nnnorm_intCast_le_one
+ nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm
+ nnnorm_mul_le_max
+ nnnorm_natCast_le_one
+ nnnorm_pow_le
+ nnnorm_prod_le_of_forall_le
+ nnnorm_zpow_le
+ norm_add_one_le_max_norm_one
+ norm_div_eq_max_of_norm_div_ne_norm_div
+ norm_eq_of_mul_norm_lt_max
+ norm_intCast_le_one
+ norm_mul_eq_max_of_norm_ne_norm
+ norm_mul_le_max
+ norm_natCast_le_one
+ norm_pow_le
+ norm_prod_le_of_forall_le_of_nonempty
+ norm_prod_le_of_forall_le_of_nonneg
+ norm_zpow_le

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.

@ghost ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jul 15, 2024
@pechersky pechersky added the WIP Work in progress label Jul 19, 2024
@ghost ghost 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 19, 2024
@pechersky pechersky removed the WIP Work in progress label Jul 23, 2024
@pechersky pechersky mentioned this pull request Jul 23, 2024
Closed
2 tasks
@pechersky pechersky added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 29, 2024
@pechersky pechersky mentioned this pull request Aug 2, 2024
Closed
4 tasks
@ghost ghost 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 5, 2024
@loefflerd
Copy link
Copy Markdown
Contributor

loefflerd commented Sep 30, 2024

@loefflerd is there a reason you marked this as blocked by the totally disconnected PR? they seem orthogonal.

Yes, there's a reason – just not a good reason! Sorry; I mistakenly thought this PR included the other one. I'll remove the flag.

@loefflerd loefflerd removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 30, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Sep 30, 2024

This PR/issue depends on:

loefflerd
loefflerd reviewed Sep 30, 2024
View reviewed changes
loefflerd
loefflerd reviewed Sep 30, 2024
View reviewed changes
@loefflerd loefflerd added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 30, 2024
@pechersky pechersky removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 1, 2024
loefflerd
loefflerd reviewed Oct 1, 2024
View reviewed changes
pechersky and others added 2 commits October 1, 2024 09:04
@pechersky
remove fintype
273071a
@pechersky @loefflerd
clarify docstring
4349689 
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
@pechersky
Copy link
Copy Markdown
Contributor Author

pechersky commented Oct 1, 2024

@loefflerd Thank you for all the feedback! It's clarifying and brings a lot of polish.

@loefflerd
Copy link
Copy Markdown
Contributor

loefflerd commented Oct 1, 2024

You're welcome, it's been a pleasure to work together on this. Let's declare it fully polished now 😄

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 1, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 1, 2024
jcommelin
jcommelin reviewed Oct 2, 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 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 2, 2024
@pechersky @urkud
feat(Analysis/Normed/{Group,Field}/Ultra): Nonarchimedean norms from …
081ccd5 
…ultrametrics (#14768)

Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 2, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Analysis/Normed/{Group,Field}/Ultra): Nonarchimedean norms from ultrametrics [Merged by Bors] - feat(Analysis/Normed/{Group,Field}/Ultra): Nonarchimedean norms from ultrametrics Oct 2, 2024
@mathlib-bors mathlib-bors bot closed this Oct 2, 2024
@mathlib-bors mathlib-bors bot deleted the pechersky/ultrametric-space-normed branch October 2, 2024 05:04
fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@pechersky @urkud @fbarroero
feat(Analysis/Normed/{Group,Field}/Ultra): Nonarchimedean norms from …
14abe69 
…ultrametrics (#14768)

Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@loefflerd loefflerd mentioned this pull request Oct 8, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@loefflerd loefflerd loefflerd left review comments

@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-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize) 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.

5 participants

@pechersky @loefflerd @mathlib4-dependent-issues-bot @jcommelin @urkud