Permission to push create branch on main mathlib repo

Stream: new members

[Oliver Nash]

What criteria does someone need to meet in order to be able to create branches on the main mathlib repo, and thus obviate the need to work from a fork?

[Oliver Nash]

I occasionally encounter very mild friction associated with maintaining a fork so if it were possible, I'd be grateful to be granted such permission. I noticed this https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/typeclass.20problems/near/184074195 a while ago as well remarks about the possibility in item 3 https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/index.md.

[Oliver Nash]

Needless to say, I absolutely understand if the maintainers feel it's best for me to continue to work from a fork and I will happily continue to do so, but it seemed like worth asking at least :-)

[Rob Lewis]

You have an invitation.

[Oliver Nash]

Oh wow, thank you very much!

[Johan Commelin]

It's great that you asked for it! We sometimes forget to give permission. For example, I was working under the assumption that you already had it. Basically, as soon as someone wants to make a 2nd PR, we usually are happy to grant permission for writing to non-master branches.