docstrings

Stream: condensed mathematics

[Kevin Buzzard]

As Johan knows, I am trying to get on top of what has been done so far so I can take more of a lead in the project now my teaching is essentially over for the year. I'm doing this by writing module docstrings for every file in the module_docstrings branch.

[Johan Commelin]

@Kevin Buzzard together with @Mario Carneiro I've been doing more work on the rescale_iso branch. We'll take care of any merge conflicts.

[Johan Commelin]

One thing that we did is moving all the rescale.lean files into a rescale/ subdirectory of src/.

[Kevin Buzzard]

I've not yet got to the murky details of the rescalings.

[Kevin Buzzard]

My branch does literally nothing other than adding module docstrings and some other files called stuff like FILES.md which contain a summary (basically written for me -- they will go stale at some point and might need to be removed) of what is happening in each directory.

[Johan Commelin]

Massive thanks to @Kevin Buzzard for writing lots and lots of docstrings all through the project. There are now also FILES.md in most directories, summarising which files are there, and what they do.