Zulip Chat Archive
Stream: PR reviews
Topic: This month in mathlib
Riccardo Brasca (Dec 01 2022 at 16:59):
I've opened #61 for the blog post about October and November. At the moment it is very WIP, and only contains PRs from October. I've been quite conservative in keeping PR, so if you're sure something shouldn't be there, please let me know.
Alex J. Best (Dec 01 2022 at 17:07):
#15405 appears twice
Riccardo Brasca (Dec 02 2022 at 09:34):
The November PRs are there.
Johan Commelin (Dec 05 2022 at 06:49):
@Riccardo Brasca Thank you so much for your help here!
Johan Commelin (Dec 05 2022 at 06:49):
I've left 3 tiny remarks. After that, let's merge this.
Riccardo Brasca (Dec 05 2022 at 09:29):
I should hit "merge pull request", right? I mean, there is no bors
Alex J. Best (Dec 05 2022 at 15:08):
PR #16053 topology/algebra/module/strong_operator, analysis/normed_space/operator_norm: strong operator topology. looks a bit funny
Riccardo Brasca (Dec 05 2022 at 15:08):
I forgot to edit the line, my fault
Riccardo Brasca (Dec 05 2022 at 15:09):
Let me merge a quick fix
Riccardo Brasca (Dec 05 2022 at 15:12):
It should be fixed
Last updated: Dec 20 2023 at 11:08 UTC