mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open j-loreaux opened this issue 3 years ago • 1 comments

Open in Gitpod

j-loreaux avatar Aug 26 '22 06:08 j-loreaux

Could you fix the conflicts?

ADedecker avatar Oct 12 '22 17:10 ADedecker

I have also added the norm_one_class and normed_algebra results.

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

ADedecker avatar Oct 15 '22 14:10 ADedecker

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.

j-loreaux avatar Oct 17 '22 13:10 j-loreaux

Thanks!

maintainer merge

ADedecker avatar Oct 19 '22 09:10 ADedecker

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

github-actions[bot] avatar Oct 19 '22 09:10 github-actions[bot]

:v: 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.

bors[bot] avatar Oct 19 '22 15:10 bors[bot]

bors merge

j-loreaux avatar Oct 24 '22 16:10 j-loreaux

Build failed (retrying...):

bors[bot] avatar Oct 24 '22 18:10 bors[bot]

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 25 '22 00:10 bors[bot]