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