pr reviewing

Stream: general

[Rob Lewis]

I'd like to second @Scott Morrison 's comment here in a more popular stream: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/88.20bottles.20of.20maths.20on.20the.20wall

Scott Morrison said:

Is 88 a new record for open PRs? Everyone is welcome to help review, whether or not you're a maintainer!

Whether it's comments on documentation or style, or suggestions for major revisions, or even just a LGTM, everything is helpful!

Contributing to mathlib isn't just about creating PRs! Checking for naming consistency, doc string spelling and grammar, "this lemma exists already," whatever you're comfortable with.