Urls in undergrad TODO

Stream: general

[Patrick Massot]

Following a conversation with @Floris van Doorn, I added in this commit the possibility to put urls in undergrad.yaml, the source of our undergrad math TODO. The idea is to clarify the intended meaning of some items, hoping this will helping improving the status of this list. #10415 is a mathlib PR adding some urls in linear algebra. Hopefully it will be merged quickly so that people can see the effect of this new feature. Then everybody should feel free to add more urls (or replace mine with better ones, I did that pretty quickly before leaving for a full teaching day).

[Eric Wieser]

Is there a matching doc-gen PR?

[Johan Commelin]

Do you mean something beyond https://github.com/leanprover-community/leanprover-community.github.io/commit/4fdd0f719774d486790accd3fb89056e19cab3f8?

[Patrick Massot]

I don't see why there would be a matching doc-gen PR.

[Eric Wieser]

Because it's hard for me to keep track of which bits of documentation are generated by what, so I named the wrong repo