Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(analysis/normed/group/basic): Earlier ℝ lemmas#16972

Closed
YaelDillies wants to merge 3 commits intomasterfrom
nnnorm_mul_to_nnreal
Closed

[Merged by Bors] - chore(analysis/normed/group/basic): Earlier ℝ lemmas#16972
YaelDillies wants to merge 3 commits intomasterfrom
nnnorm_mul_to_nnreal

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies commented Oct 14, 2022 •
edited
Loading

Move lemmas about the norm on ℝ from analysis.normed.field.basic to analysis.normed.group.basic.

This avoids having to import normed_field to use real.norm_of_nonneg.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) labels Oct 14, 2022
@YaelDillies YaelDillies mentioned this pull request Oct 14, 2022
Closed
2 tasks
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Oct 15, 2022

This is probably sensible, but can you add a justification to the PR description?

@YaelDillies
Copy link
Copy Markdown
Collaborator Author

YaelDillies commented Oct 15, 2022

Done!

@ocfnash ocfnash added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 24, 2022
@ocfnash
Copy link
Copy Markdown
Collaborator

ocfnash commented Oct 24, 2022

I agree this is probably a good idea. I note there is now a merge conflict however.

@YaelDillies YaelDillies removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 28, 2022
@mcdoll
Copy link
Copy Markdown
Member

mcdoll commented Oct 29, 2022

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 29, 2022

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

@mcdoll mcdoll changed the title move(analysis/normed/group/basic): Earlier ℝ lemmas chore(analysis/normed/group/basic): Earlier ℝ lemmas Oct 29, 2022
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Oct 29, 2022

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 29, 2022
bors bot pushed a commit that referenced this pull request Oct 29, 2022
@YaelDillies
chore(analysis/normed/group/basic): Earlier ℝ lemmas (#16972)
be61b02 
Move lemmas about the norm on `ℝ` from `analysis.normed.field.basic` to `analysis.normed.group.basic`.

This avoids having to import `normed_field` to use `real.norm_of_nonneg`.
@bors
Copy link
Copy Markdown

bors bot commented Oct 29, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(analysis/normed/group/basic): Earlier ℝ lemmas [Merged by Bors] - chore(analysis/normed/group/basic): Earlier ℝ lemmas Oct 29, 2022
@bors bors bot closed this Oct 29, 2022
@bors bors bot deleted the nnnorm_mul_to_nnreal branch October 29, 2022 11:27
@eric-wieser eric-wieser added the hacktoberfest-accepted Without this label hacktoberfest is scared off by bors label Oct 29, 2022
@YaelDillies YaelDillies mentioned this pull request Oct 30, 2022
Closed
7 tasks
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

hacktoberfest-accepted Without this label hacktoberfest is scared off by bors ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@YaelDillies @eric-wieser @ocfnash @mcdoll @sgouezel