Using MSC identifiers in mathlib

Stream: general

[Scott Morrison]

194 missing module docstrings!

[Scott Morrison]

All listed at https://github.com/leanprover-community/mathlib/blob/master/scripts/style-exceptions.txt if anyone wants to tackle a few!

[Johan Commelin]

@Yaël Dillies has been making several PRs with module docstrings lately. Thanks a lot for that!

[Yaël Dillies]

Having to revise for exams gives me documentation energy :sweat_smile:

[Sebastian Reichelt]

Mario Carneiro said:

I usually find wikipedia links to be significantly more helpful than MSC codes

It would be great to have a Wikipedia link in every docstring because such a link could also be used as a key into a database of definitions and theorems. I wrote a proposal about this here: https://github.com/SReichelt/slate/discussions/84. If the Wikipedia links are already in the source code, that would be the best of the different variants described there, because the database could be updated automatically by regularly scraping the mathlib docs.