Zulip Chat Archive

Stream: new members

Topic: Golfing int.not_is_field

Aresh Pourkavoos (Mar 04 2022 at 23:42):

Hi, I'm Aresh and I'm a CS undergrad at Carnegie Mellon! I got here from the Xena project Discord server, whose members suggested that I should submit a mathlib PR for golfing the proof of the lemma that the integers are not a field. David Ang and Eric R. shortened the proof further.

Mauricio Collares (Mar 05 2022 at 00:21):

Welcome! I believe the mathlib maintainers will need your GitHub username so you can push to non-master branches (for CI reasons, submitting a PR from a fork is discouraged in mathlib)

Aresh Pourkavoos (Mar 05 2022 at 00:30):

It's Aresh-P. Thank you!

Bryan Gin-ge Chen (Mar 05 2022 at 00:32):

Aresh Pourkavoos said:

It's Aresh-P. Thank you!

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

Aresh Pourkavoos (Mar 07 2022 at 20:04):

I submitted the PR and accepted Eric Weiser's changes, but it's still marked "awaiting-author." Is there anything else I need to do before it's merged?
https://github.com/leanprover-community/mathlib/pull/12451

Ruben Van de Velde (Mar 07 2022 at 20:09):

You have you change the label back yourself

Aresh Pourkavoos (Mar 07 2022 at 20:10):

Just did, thanks

Aresh Pourkavoos (Mar 07 2022 at 20:12):

Should I add "awaiting-review?"

Moritz Doll (Mar 08 2022 at 03:12):

yes, see https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr

Last updated: Dec 20 2023 at 11:08 UTC