PRs from new contributors

Stream: PR reviews

[Michael Rothgang]

In light of #11658, I just looked over ~all relevant PRs and tagged with new-contributor as needed.
(I checked everybody who requested github permissions since September. This might not be fool-proof, but is probably good enough.)

This means the #queue now contains many more PRs tagged new-contributor. You may consider to give those a look :-)

[Johan Commelin]

Thanks for your help!

[Michael Rothgang]

I just approved #11640. Does anybody want to take a look?
Short and simple (introduces a lemma about functions to golf a proof in topology); no topology knowledge needed to review. Just two small style questions on which I'd appreciate a second pair of eyes. And obvious, I don't have approval rights :-)

[Michael Rothgang]

This was filed two days ago - this could be a speedy review to a new contribution!

[Michael Rothgang]

And #11626 is also basically good to go, from my side.