permission to push to GitHub

Stream: new members

[Scott Morrison]

Hi, I'm pretending to be a new user who wants to make a pull request to mathlib. Could someone please give me permission to push a branch?

[Johan Commelin]

Hey Scott, sure! One second.

[Scott Morrison]

Oh --- my username is semorrison

[Johan Commelin]

Ok, you should have an invitation email.

[Johan Commelin]

Yeah, I figured that out (-;

[Apurva Nakade]

Hi, I'm working on some linear algebra theorems to mathlib (hoping to get to Spectral theorem) and need to make a pull-request to add documentation to linear_algebra/direct_sum_module and close #3418. Could I get permission to push a branch? My Github username is apurvnakade

[Bryan Gin-ge Chen]

@Apurva Nakade https://github.com/leanprover-community/mathlib/invitations

[Apurva Nakade]

Thank you!

[Frederick Eidsnes Thøgersen]

Hi, I am a "semi-new" user currently following Scott Morrison's tutorial. I have a project with Professor Buzzard with regards to local fields. The last two months, I have just been practicing Lean, but I now plan to start making some pull requests to mathlib. Would it be possible to request that someone may give me permission to push a branch? I believe my git username is: FrederickThogersen

[Scott Morrison]

@Frederick Eidsnes Thøgersen, done!

[Frederick Eidsnes Thøgersen]

Thank you very much :+1:

[Kenji Nakagawa]

Hi, I'm working on some ring theory things, such as a third Noetherian definition, and adding a few facts about integral domains (and hopefully eventually dedekind domain things). Can I get permission to push a branch? My github username is mushokunosora

[Bryan Gin-ge Chen]

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

[Kenji Nakagawa]

Thanks!

[Jia Ming]

Hello! I'm snooping around order.lattice and thought I could make some small improvements, may I have permission to push a branch to mathlib? My username is jiaminglimjm

[Bryan Gin-ge Chen]

@Jia Ming invite sent! https://github.com/leanprover-community/mathlib/invitations

[Jia Ming]

Thank you!

[Patrick Massot]

You should discuss a bit your improvement ideas here before spending too much time coding, just to make sure you won't waste time.

[Jia Ming]

Ah right, noted, i was just too excited hahah. It's a really small change, so i hope i dont waste anyone else's time too much

[Patrick Massot]

Oh I meant your time.

[Patrick Massot]

I don't want you to invest too much time only to find out that what you had in mind is already in mathlib somewhere or undesirable for some reason.

[Riccardo Brasca]

Hi all, can I have permission to push to github? My username is riccardobrasca

Thank you!

[Bryan Gin-ge Chen]

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

[Riccardo Brasca]

Thank you!

[Kevin Buzzard]

Hi. Can Imperial undergrad Xiang Li, github userid Lix0120, have push access to non-master branches?

[Bryan Gin-ge Chen]

@Kevin Buzzard Access given!

[Cedric Holle]

Hi, I'm Cedric from Saarbrücken, Germany. I would like to make a pull request to mathlib. Could someone please give me permission to push a branch?
Github-account: todbeibrot

[Riccardo Brasca]

Done!

[Suhas Kotha]

Hello, I'm trying to prove a few combinatorial identities! Could I get permission to push a branch? My username is kothasuhas

[Kevin Buzzard]

What are you trying to prove? You can just make your own repository and prove them there if it's just a small project. But maybe they're appropriate for mathlib.

[Suhas Kotha]

I have written a proof of the hockey stick identity and was wondering if I could push it since my preliminary search did not find it (https://www.wikiwand.com/en/Hockey-stick_identity)

[Eric Wieser]

I assume docs#nat.choose_succ_succ is a different statement? (Edit: yes)

[Patrick Luo]

hello may I have permission to push to github? my username is m3hgu5t4

[Johan Commelin]

@Patrick Luo https://github.com/leanprover-community/mathlib/invitations

[Matias Heikkilä]

Hello world! I recently got introduced to lean, and in the long term I'd like to contribute to mathlib. Requesting push permission to GH. My username is mapehe

[Johan Commelin]

@Matias Heikkilä Can you share a bit about your background and the kind of stuff you would like to contribute?

[Johan Commelin]

Do you already have some lean code that you would like to PR?

[Matias Heikkilä]

Sure @Johan Commelin . I did a PhD in probability and statistics -related things a few years ago and I've been working as a software developer since. I don't have any lean code yet: I thought it would be better to approach the people first and see how things work around here. Ideally I'd like to find a small corner somewhere that could be improved and make some PRs related to that. Some topics that could interest me are probability theory, measure theory and topology.

[Johan Commelin]

@Matias Heikkilä Welcome. Here's an invitation: https://github.com/leanprover-community/mathlib/invitations

[Chase Fleming]

Greetings, I'd like to have permission to push a branch. I'm attempting to expand topology/separation. My GitHub username is flemingchase.

[Markus Himmel]

@Chase Fleming I sent you an invitation: https://github.com/leanprover-community/mathlib/invitations

[Matthias U]

Hi, I've been working on an implementation of amenable groups. Could I get permission to push to the mathlib? My username is matthias567

[Johan Commelin]

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

[Archie]

Hi - i'm a new user - would i be able to have push access to a mathlib branch? my github username is archiebrowne . Thanks.

[Anne Baanen]

Archie said:

Hi - i'm a new user - would i be able to have push access to a mathlib branch? my github username is archiebrowne . Thanks.

Hi! Can you share a bit about your background and the kind of stuff you would like to contribute? (In particular, I assume you are working in Lean 4?)

[Archie]

Hi - yeah so i'm an undergrad at Imperial currently doing a research project, I would like at the moment to add only one small addition - the function:

def Int.modEq_sub_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a - n * c ≡ b [ZMOD n] := by sorry

without the sorry - to compliment the already existing 'Int.modEq_add_fac'

Thanks

[Anne Baanen]

Thank you, invitation sent! https://github.com/leanprover-community/mathlib4/invitations

[Archie]

Thanks :))

[Noam Atar]

Hey, I wrote a bit of lean code about two years ago. I want to return, and add content to mathlib4. Can I get permissions to push branches there? My github username is atarnoam

[Scott Morrison]

Hi Noah, as above, could you say something about your background, and something about the sort of thing you're planning to contribute?

[Noam Atar]

Sure. I study for an MSc in math at Tel Aviv University. I like representation theory of top. groups, and would like to expand on it, eventually. For now, I just want to define the modular function of a group :)

[Scott Morrison]

@Noam Atar, please see https://github.com/leanprover-community/mathlib4/invitations

[Noam Atar]

Thanks!

[Pedro Sánchez Terraf]

Hi (once again!). I already have branch-push access to mathlib3. In order to restart my PR process, I think that I should ask again for Mathlib4, is this right? I'm sterraf

[Ruben Van de Velde]

Pedro Sánchez Terraf said:

Hi (once again!). I already have branch-push access to mathlib3. In order to restart my PR process, I think that I should ask again for Mathlib4, is this right? I'm sterraf

@maintainers

[Riccardo Brasca]

Invitation sent!

[Martin Dvořák]

Hi! I'd like to get permission to push to Mathlib4.

[Scott Morrison]

@Martin Dvořák, please see https://github.com/leanprover-community/mathlib4/invitations

[Peiran Wu]

Hello again! I'm a PhD student in permutation group theory at the University of St Andrews. I have access to mathlib3 but I'm getting ready to make some new PRs to mathlib4, on group actions. I'll start with pointwise stabilizers, but I'll also add Subgroup.IsMaximal Subgroup.Normal.IsMaximal AddSubgroup.IsMaximal (analogously to Ideal.IsMaximal) since I'll be using at least two of these further down the line. Could someone please invite me (GitHub handle wupr)?

[Peiran Wu]

(deleted)

[Jireh Loreaux]

@Peiran Wu invitation sent: https://github.com/leanprover-community/mathlib4/invitations

[Notification Bot]

7 messages were moved from this topic to #new members > stabilizers and maximal subgroups by Jireh Loreaux.

[Uni Marx]

Hi, I'm a math undergrad in Erlangen, Germany and would like to contribute to mathlib - at the moment there's a couple identities and propositions about bundled relations I'd like to add. My username is uniwuni

[Alex J. Best]

@maintainers not sure if the message above was missed

[Jireh Loreaux]

@Uni Marx please see: https://github.com/leanprover-community/mathlib4/invitations

[Uni Marx]

Thanks!