mathlib permission?

Stream: maths

[fzyzcjy]

Hi friends, I am making a tiny PR to fix a tiny typo (https://github.com/leanprover-community/mathlib/pull/17552) and a mathlib collaborator said I should ask for permission in Zulip. Not sure whether I should ask here :)

[Alex J. Best]

The full instructions are at https://leanprover-community.github.io/contribute/index.html. One of the @maintainers will grant you permission for future PRs, I think your original one should be reviewable as it is only small, but you should follow the instructions there for future prs.

[fzyzcjy]

Thank you!