Zulip Chat Archive

Stream: new members

Topic: github access

Carlos Caralps (Apr 14 2021 at 10:41):

Hi there, I’m a math student. Last months I’ve been learning Lean being a participant of the Barcelona Lean Seminar. In this seminar we have focused our work in topological spaces with Lean and I’ve done some lemes about separation axioms.
I’d like to ask for permission to push to non-master branches of mathlib. I’d like to do my first PR with those lemmas.

Kevin Buzzard (Apr 14 2021 at 10:42):

Your github userid is carloscaralps? Nice stuff! Is this being run by Marc?

Markus Himmel (Apr 14 2021 at 10:43):

I sent you an invite, it should appear at https://github.com/leanprover-community/mathlib/invitations

Carlos Caralps (Apr 14 2021 at 10:45):

Yes, my userid is carloscaralps and @Marc Masdeu is running the seminar

Carlos Caralps (Apr 14 2021 at 10:47):


Kevin Buzzard (Apr 14 2021 at 10:51):

Great! I did some stuff with topological spaces with my students a couple of months ago: https://xenaproject.wordpress.com/2021/02/10/formalising-mathematics-workshop-4/

Marc Masdeu (Apr 14 2021 at 10:59):

Kevin, we are aware of your TCC workshops, the blog posts are extremely useful (at least to me). We did some basics (up to compacity and separation, you can see it at github.com/mmasdeu/barcelonaleanseminar), and one goal is to make the Topology Game. Right now, we decided to stop building topological spaces from scratch (we gave up when trying to prove that the Moebius band defined as a quotient of a square is homeomorphic to the strip as a subspace of R3), and move on to adapting all that we have to the Game.

Kevin Buzzard (Apr 14 2021 at 11:06):

Thanks for the link!

Patrick Massot (Apr 14 2021 at 13:56):

I can believe there are missing lemmas about the zoo of separation conditions in mathlib. However I'm a bit worried that the proof you will have won't blend nicely with mathlib if you didn't use filters all over the place.

Jon Eugster (May 22 2021 at 18:13):

I would like to get into contributing to mathlib, could I get permission to push to a non-master branch? My username is joneugster.

I thought my first PR could be small contributions about fraction rings, like instance fraction_ring.char_zero [h: char_zero R]: char_zero (fraction_ring R) as they should be very quick to review.

Johan Commelin (May 22 2021 at 18:22):

@Jon Eugster Voila: https://github.com/leanprover-community/mathlib/invitations

Jon Eugster (May 22 2021 at 18:27):

thank you!

Jon Eugster (May 24 2021 at 08:32):

Is it better to discuss mathlib PRs here on Zulip (i.e. file sturcture, generality) or to make a PR get feedback and refactor it afterwards?

Kevin Buzzard (May 24 2021 at 08:33):

If you're new to the PR process then there will be no harm in discussing potential PR's here.

Kevin Buzzard (May 24 2021 at 08:34):

But there is also no harm in making the PR and then starting a thread about it in #PR reviews . However if the PR costs hours of your time and then is instantly met with a "oh no we can't do it like that at all, for the following technical reason" then this would be a bit grim

Scott Morrison (May 24 2021 at 09:45):

The #PR reviews stream is also extremely useful if you don't get comments on your PR... Sometimes the queue exceeds our ability to shepherd it along, but lots of us are compulsively helpful here on zulip. :-)

Jon Eugster (May 24 2021 at 09:53):

ok so I have a few questions about starting with mathlib PRs. I would like mathlib to know automatically that the characteristics of the fraction_ring R of an integral domain is the same as the char. of R. Something like:

import algebra.char_p.basic
import ring_theory.localization

namespace fraction_ring

variables (R: Type*) [integral_domain R] (p: )

instance char_p [h: char_p R p]: char_p (fraction_ring R) p := sorry

instance char_zero [h: char_zero R]: char_zero (fraction_ring R) := char_p.char_p_to_char_zero (fraction_ring R)

The main ingredient is that the algebra map R →+* fraction_ring R is injective for an integral domain, which is (fraction_map.injective (fraction_ring.of R))

  • I could see this be stated in different generalities:
    1) as above
    2) have the injectivity as an instance for the fraction_ring case and state the above for commutative rings/algebras with this injectivity assumption.
    3) go into the definition of a fraction_ring (i.e. look at localization.r) and prove it there.

  • I could also see multiple places to locate this:
    1) a new file algebra/char_p/localization.lean
    2) in ring_theory/localization.lean (but seems silly to import char_p there)
    3) ring_theory/localization.lean is about 1700 lines long, the last 30 thereof defining fraction_ring, at which point does it make sense to split this up into ring_theory/localization/basic.lean and ring_theory/localization/fraction_ring.lean?

Any recommendations?

Scott Morrison (May 24 2021 at 10:01):

I don't know this part of the library well, but I'll just say one thing: while splitting up large files (particularly where this significantly reduces imports to one or more chunks) is a good and valuable thing to do, it's often best to do it as a separate PR, either before or after the "content" PR, as it's much easier to review the content if we don't have to wade through the "just moving stuff" diffs.

Scott Morrison (May 24 2021 at 10:02):

Perhaps if this is your first PR it's safest to start off with using a new file, and then we'll remind you to move parts (or perhaps all) to other homes.

Scott Morrison (May 24 2021 at 10:03):

Certainly don't go with 2) --- adding new imports to already big files is a pain.

Ender Doe (Aug 08 2021 at 22:31):

Hello :wave:, I have being working on formalizing the thomaes function with help from the Xena Discord, and along the way I think I have some lemmas worth PRing to mathlib.

I have been following this guide https://www.youtube.com/watch?v=Bnc8w9lxe8A, and am here to request credentials to push a branch.

Here is my GitHub account https://github.com/FrickHazard, cheers and thank you.

Bryan Gin-ge Chen (Aug 08 2021 at 22:32):

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

Paul Lezeau (Aug 10 2021 at 15:24):

Hi ! :wave:
I'm working on formalizing some algebraic number theory, and I have a few lemmas I'd like to PR to mathlib. Would it be possible to get PR access ? My GitHub username is Paul-Lez.
Thanks a lot !

Anne Baanen (Aug 10 2021 at 15:30):

Hi! :wave: I tried to give you access, but I got an error 500. Maybe you already got the invite before GitHub broke?

Paul Lezeau (Aug 10 2021 at 15:32):

I'll have a look. Where can I find invitations I have received on GitHub ?

Anne Baanen (Aug 10 2021 at 15:32):

In your notifications I believe: https://github.com/notifications

Anne Baanen (Aug 10 2021 at 15:34):

What areas of algebraic number theory are you interested in? We are currently working on merging a proof of the finiteness of the class number in a number ring.

Paul Lezeau (Aug 10 2021 at 15:34):

Oh ok ! Well I haven't received any invite.

Alex J. Best (Aug 10 2021 at 15:35):

I'm also having issues with github right now, so probably its a global thing?

Anne Baanen (Aug 10 2021 at 15:36):

Just tried for a third time, looks like I can't make it work :(

Eric Wieser (Aug 10 2021 at 15:37):


Anne Baanen (Aug 10 2021 at 15:37):

Oh yeah, https://www.githubstatus.com/ is reporting a lot of issues

Paul Lezeau (Aug 10 2021 at 15:37):

Anne Baanen said:

What areas of algebraic number theory are you interested in? We are currently working on merging a proof of the finiteness of the class number in a number ring.

I'm working on formalizing Dedekind's theorem on factoring ideals (p)(p) in the ring of integers of a number field (under @Damiano Testa's supervision). It's great that you've already done so much !

Anne Baanen (Aug 10 2021 at 15:39):

Oh, that would be a great addition!

Anne Baanen (Aug 10 2021 at 15:40):

(Did another of the @maintainers already try giving Paul-Lez access?)

Bryan Gin-ge Chen (Aug 10 2021 at 16:45):

I think I managed to send an invitation just now: https://github.com/leanprover-community/mathlib/invitations @Paul Lezeau

Paul Lezeau (Aug 10 2021 at 16:51):

That worked, thanks a lot !

Kevin Buzzard (Aug 11 2021 at 06:41):

@Paul Lezeau A useful theorem to have would be proving that if L/KL/K is a finite extension of number fields and PP is a prime of OK\mathcal{O}_K then POLP\mathcal{O}_L factors as I=1gQiei\prod_{I=1}^gQ_i^{e_i} with ieifi=[L:K].\sum_ie_if_i=[L:K].

Paul Lezeau (Aug 11 2021 at 07:33):

A while back, you mentioned this could be obtained as a corollary of the result :
Kevin Buzzard said:

Here is something I would very much like to have in Lean: if L/KL/K is a finite extension of global fields and PP is a prime of KK which splits as iQiei\prod_iQ_i^{e_i} in LL then KPKL=iLQiK_P\otimes_KL=\bigoplus_iL_{Q_i} for some value of == (probably ≃+*).

I'd be happy to work on it once I'm done with Dedekind's theorem. Do you have any references where I could find the proof ?

Kevin Buzzard (Aug 11 2021 at 07:44):

My post-doc Maria is thinking about adeles in Lean and she is going to need this kind of thing too, but this stream probably isn't the best place to talk about technicalities (it's about GitHub access). My instinct with global fields by the way is to not attempt to unify the definition and work with number fields and function fields separately. The proof I know of the completion result is in Cassels-Froelich.

Last updated: Dec 20 2023 at 11:08 UTC