subfolder README.md's

Stream: mathlib4

[Mario Carneiro]

Riccardo Brasca said:

Well, it is surely strange that there is a file, Mathlib/Algebra/README.md, that basically nobody knows about and that contains an hard rule.

I want to echo this and make a thread to discuss it, because AFAIK we have never used README.md files in subfolders, and we should make a policy about this (use it consistently or not at all).

[Robin Carlier]

I'm voting in favor of using them consistently.

[Jz Pan]

I think there was a thread discussing doc-gen support for README.md

[Jz Pan]

#general > RFC: Explaining folder content @ 💬

[Robin Carlier]

If the goal of these readmes is to contain development lore, I think it's OK if they're not included in the user documentation (which I feel is what doc-gen generates)