Missing module docstrings + type_of% theorem links

[mo271]

No description provided.

[YaelDillies]

Could we reduce the maintenance load by not duplicating the module docs?

[mo271]

My feeling is that right now that affects really only quite a few problems and before this pull request it was incosistent: sometime we had an extra module doc other files were just empty other than one line of import.
I changed the fewer files so that now every file has exactly one module docstring.
But I'm happy also to go the other way: but then for some of them it is a bit awkward to include both the formulation from Wikipedia and the one from erdosproblems.com (for instance).
I think the important thing is to make the problems findable: so good to have strings like "Hadwiger" both inside the files, but perhaps also good have them as filenames.

If we decide to do it differently I suggest to create an issue or just do it as a follow up? This doesn't affect the "WrittenOnTheWall" stuff here.

[YaelDillies]

My concern is to reduce maintenance burden as much as possible. What about we make the module docs of the mirror files be just "This file points to the canonical formalization in"? I believe variations of the same problem should be discussed within a single file, rather than the discussion being split across several files.

[mo271]

My concern is to reduce maintenance burden as much as possible. What about we make the module docs of the mirror files be just "This file points to the canonical formalization in"? I believe variations of the same problem should be discussed within a single file, rather than the discussion being split across several files.

Will do that in a follow up

[mo271]

#3608