Zulip Chat Archive

Stream: mathlib4

Topic: porting Algebra/Quotient

Siddhartha Gadgil (Nov 18 2022 at 11:06):

Created PR https://github.com/leanprover-community/mathlib4/pull/643 (a little hastily as I have not yet figured out how to avoid work duplication).

Riccardo Brasca (Nov 18 2022 at 11:08):

Please update the wiki, otherwise other people will start working on the same file.

Kevin Buzzard (Nov 18 2022 at 12:15):

I did this because it still wasn't done and I regarded it as critical.

Siddhartha Gadgil (Nov 18 2022 at 12:30):

Kevin Buzzard said:

I did this because it still wasn't done and I regarded it as critical.

Thanks. I don't have permission for the Lean 3 repository so could not do it.

Siddhartha Gadgil (Nov 18 2022 at 12:30):

Can I get the permission for the future?

Riccardo Brasca (Nov 18 2022 at 12:32):

What is your github username?

Siddhartha Gadgil (Nov 18 2022 at 12:33):

siddhartha-gadgil

Riccardo Brasca (Nov 18 2022 at 12:34):

I've sent an invitation. (I am afraid you need to find another reviewer for your mathlib4 PR, I am a beginner in Lean4.)

Siddhartha Gadgil (Nov 18 2022 at 12:39):

Thanks. I got the invitation.
@Riccardo Brasca I requested you as a reviewer at Github's suggestion :)

Last updated: Dec 20 2023 at 11:08 UTC