mathlib push access

Stream: general

[Kevin Buzzard]

@Simon Hudon or @Rob Lewis or whoever else can do this -- can @Jason KY. have push access to non-master branches of mathlib? His github UID is JasonKYi

[Rob Lewis]

Invitation sent.

[Bendit Chan]

@maintainers Hello, I am a student of @Kevin Buzzard at Imperial, interested in working on Newton's identities. Can I have push access to non-master branches of mathlib? My github ID is blastzit. Thanks.

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Gareth Ma]

(deleted)

[Gareth Ma]

Hi, I would like to work on mersenne numbers, in particular moving them into a separate file and prove results about them, most notably the Euclid-Euler Theorem (it exists already, so I will just move the result from archive/100-theorems-list/70_perfect_numbers.lean), and also that nat.prime mersenne n \imp nat.prime n, and some useful lemmas for casting between nat.mersenne and int.mersenne. I will also have to modify the lucas_* files that use the mersenne definitions. Can I have the relevant permission, which I think is writing to non-master branch? Thank you!

My GitHub username is @grhkm21.

[Kevin Buzzard]

@maintainers

[Gareth Ma]

Hello :"

[Kevin Buzzard]

I'm confused why I pinged maintainers in this thread. Sorry!

[Gareth Ma]

I still don't have permissions, or at least I think so. When I click on the mathlib/invitations link above, it says I am not invited yet

[Johan Commelin]

@Gareth Ma Sorry, should work now: https://github.com/leanprover-community/mathlib4/invitations

[Junyan Xu]

mathlib4?

[Johan Commelin]

oops

[Johan Commelin]

@Gareth Ma next attempt: https://github.com/leanprover-community/mathlib/invitations