Add comments about what is in scope for mathlib

[kbuzzard]

I think it would be slightly nicer to have a link to say "here is a big list of projects which depend on mathlib, please consider joining them", but right now this is waiting on leanprover/reservoir#49 . For now, I just link to the reservoir home page.

[fpvandoorn]

I think this is generally a good change, so let's get this in!
I have 2 comments.

[fpvandoorn]

Actually, a third comment: Your discussion is only relevant when adding completely new things to Mathlib, while the page is about any Mathlib contributions (including small fixes or single-lemma additions). So it should be made clear that your new section doesn't always apply (and maybe the section should be later?)

[kbuzzard]

I have added "One example of such a repository is the combinatorial game
theory repository." (lines 48-49) when referring to the possibility of a standalone
repo depending on mathlib. But I am not aware of a link to this repo yet.
Should I remove this comment? Should I add the FLT repo or Carleson as examples?
These are a bit different because for both repos I can imagine some of the material
being upstreamed to mathlib, where with CGT we seem to have made a decision to
keep the repo separate.

[PatrickMassot]

I think the link is https://github.com/YaelDillies/add-combi but of course you should check with Yaël before writing anything about that project.