month in mathlib (oct 2021)

Stream: general

[Johan Commelin]

Recently we've started writing overview blogposts of what has happened in mathlib in the past month. See https://leanprover-community.github.io/blog/categories/cat_month-in-mathlib/.
Since it's the first of the month, it's time for a new edition. blog#16 is the raw input that I've gathered so far. If you think I've missed an interesting PR, please point that out. If you have 3 or 4 lines of commentary that you want to write about a PR (or block of PRs) please post them here or add them as suggestion to blog#16.

[Yaël Dillies]

That's when you notice you're a backstage maintainer and haven't added any cool maths to mathlib in a month :sad:

[Johan Commelin]

I think that's what happens to many of us

[Johan Commelin]

There were over 400 PRs, but these blogposts are a way to draw attention to highlights for outsiders. Many of the technical refactors are very important but you need to be an insider to understand the "before -- after" of those refactors.

[Yaël Dillies]

Yeah. Locally finite orders turn out very useful but you can't just say to the outside world "We've finally defined finite intervals!"

[Johan Commelin]

I should add that even some of the stuff that is currently on the list might still be pruned away.

[Johan Commelin]

I think it's best to have a pretty short list of substantial highlights.

[Yaël Dillies]

Yeah, for example I don't think we need 4 entries for Besicovitch.

[Johan Commelin]

That will become 1 entry (but it might mention 3 or 4 PR numbers)

[Johan Commelin]

I need to run again. Family visit.

[Oliver Nash]

Yaël Dillies said:

That's when you notice you're a backstage maintainer and haven't added any cool maths to mathlib in a month :sad:

FWIW @Yaël Dillies I wish I was half as productive as you or had known half as much mathematics as you do when I was your age.

[Johan Commelin]

I pushed a bit of commentary.

[Yaël Dillies]

Oliver Nash said:

FWIW Yaël Dillies I wish I was half as productive as you or had known half as much mathematics as you do when I was your age.

Now that's compliment :blush:

[Johan Commelin]

I've integrated the suggestions by @Kyle Miller and @Heather Macbeth