Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - refactor(analysis/normed/group/basic): generalize (semi)normed_group.induced to monoid_hom_class and add more tools to pull back norm structures #16255

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - refactor(analysis/normed/group/basic): generalize (semi)normed_group.induced to monoid_hom_class and add more tools to pull back norm structures #16255

wants to merge 5 commits into from

Conversation

j-loreaux
Copy link
Collaborator

Open in Gitpod

@j-loreaux j-loreaux added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 26, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 30, 2022
@j-loreaux j-loreaux changed the title refactor(analysis/normed/group/basic): generalize (semi)normed_add_comm_group.induced to add_monoid_hom_class refactor(analysis/normed/group/basic): generalize (semi)normed_add_comm_group.induced to add_monoid_hom_class and add more tools to pull back norm structures Aug 30, 2022
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 30, 2022
ADedecker
ADedecker reviewed Aug 30, 2022
View reviewed changes
Copy link
Member

@ADedecker ADedecker left a comment

Choose a reason for hiding this comment

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

Could you also add instances about how norm_one_class and normed_algebra behave under these pull backs? (Presumably you'll need stronger assumptions than non_unital_ring_hom_class of course)

src/analysis/normed/field/basic.lean Show resolved Hide resolved
@dupuisf dupuisf added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 3, 2022
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 7, 2022
@ADedecker
Copy link
Member

Could you fix the conflicts?

@ADedecker ADedecker self-assigned this Oct 12, 2022
@ADedecker ADedecker added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 12, 2022
@j-loreaux j-loreaux force-pushed the j-loreaux/induced-norm-hom-class branch from bad493b to f5aec15 Compare October 14, 2022 05:08
@j-loreaux j-loreaux added awaiting-CI The author would like to see what CI has to say before doing more work. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Oct 14, 2022
@j-loreaux j-loreaux changed the title refactor(analysis/normed/group/basic): generalize (semi)normed_add_comm_group.induced to add_monoid_hom_class and add more tools to pull back norm structures refactor(analysis/normed/group/basic): generalize (semi)normed_group.induced to monoid_hom_class and add more tools to pull back norm structures Oct 14, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Oct 14, 2022
@ADedecker
Copy link
Member

I have also added the norm_one_class and normed_algebra results.

Sorry, I don't see them 😅 Git mistake maybe?

@j-loreaux
Copy link
Collaborator Author

I have also added the norm_one_class and normed_algebra results.

Sorry, I don't see them sweat_smile Git mistake maybe?

I knew I wasn't crazy. I did do this, it was just on my work machine, so maybe I never pushed? I checked the diff on GitHub; they are definitely present now.

ADedecker
ADedecker approved these changes Oct 18, 2022
View reviewed changes
Copy link
Member

@ADedecker ADedecker left a comment

Choose a reason for hiding this comment

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

I left one last nitpick, everything else looks good to me

src/analysis/normed/field/basic.lean Show resolved Hide resolved
@ADedecker ADedecker removed the awaiting-review The author would like community review of the PR label Oct 18, 2022
@ADedecker ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 18, 2022
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 18, 2022
@ADedecker
Copy link
Member

Thanks!

maintainer merge

@github-actions
Copy link

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

dupuisf
dupuisf reviewed Oct 19, 2022
View reviewed changes
Copy link
Collaborator

@dupuisf dupuisf left a comment

Choose a reason for hiding this comment

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

Just one quibble about a possibly missing @[reducible].

bors d+

src/analysis/normed/field/basic.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Oct 19, 2022

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

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 19, 2022
@j-loreaux
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Oct 24, 2022
@j-loreaux
refactor(analysis/normed/group/basic): generalize `(semi)normed_group…
48e8de0 
….induced` to `monoid_hom_class` and add more tools to pull back norm structures (#16255)
@bors
Copy link

bors bot commented Oct 24, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Oct 24, 2022
@j-loreaux
refactor(analysis/normed/group/basic): generalize `(semi)normed_group…
fe67b48 
….induced` to `monoid_hom_class` and add more tools to pull back norm structures (#16255)
@bors
Copy link

bors bot commented Oct 25, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(analysis/normed/group/basic): generalize (semi)normed_group.induced to monoid_hom_class and add more tools to pull back norm structures [Merged by Bors] - refactor(analysis/normed/group/basic): generalize (semi)normed_group.induced to monoid_hom_class and add more tools to pull back norm structures Oct 25, 2022
@bors bors bot closed this Oct 25, 2022
@bors bors bot deleted the j-loreaux/induced-norm-hom-class branch October 25, 2022 00:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dupuisf dupuisf dupuisf left review comments

@ADedecker ADedecker ADedecker approved these changes

Assignees

@ADedecker ADedecker

Labels
delegated The PR author may merge after reviewing final suggestions. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@j-loreaux @ADedecker @dupuisf @leanprover-community-bot-assistant