Zulip Chat Archive

Stream: new members

Topic: Is this worth contributing to mathlib?


view this post on Zulip Devon Tuma (Jul 09 2020 at 00:19):

I started writing some proofs about Jacobson rings as a way to get a feel for how algebraic things in Lean work, and I'm curious if there would be any interest in adding them to mathlib at all?
I'd like to avoid doing too much refactoring later, so if there is interest I'd like to start being more careful to keep the proofs and theorems more clean and consistent.

view this post on Zulip Jalex Stark (Jul 09 2020 at 01:42):

without knowing much algebra myself, this sounds like the kind of thing that ought to end up in mathlib.

view this post on Zulip Jalex Stark (Jul 09 2020 at 01:43):

you can read this guide to see what the process is like
https://leanprover-community.github.io/contribute/index.html

view this post on Zulip Scott Morrison (Jul 09 2020 at 03:20):

Yes, these certainly belong in mathlib!

view this post on Zulip Johan Commelin (Jul 09 2020 at 04:04):

@Devon Tuma Quick check: did you notice that we already have the Jacobson radical:

src/ring_theory/ideal_operations.lean:def jacobson (I : ideal R) : ideal R :=

It would be sad if you are duplicating that part of the theory.

view this post on Zulip Devon Tuma (Jul 09 2020 at 04:10):

Yes, I'm actually using that for this, perhaps the terminology isn't great but a "Jacobson ring" is defined in terms of the "Jacobson radicals" already in mathlib. One of the equivalent definition of it for a ring would be ∀ (I : ideal R), I = I.radical → I = I.jacobson.

view this post on Zulip Devon Tuma (Jul 09 2020 at 04:11):

Although I see I maybe misunderstood and your totally aware of what I just said. In which case yes I'm building off the existing parts of the theory in mathlib

view this post on Zulip Yury G. Kudryashov (Jul 09 2020 at 11:07):

Hint: you don't have to wait till you have an "interesting" result before opening the first PR.

view this post on Zulip Devon Tuma (Jul 10 2020 at 04:21):

Is someone able to give me rights to push a branch for this to mathlib on github? My github username is 'dtumad'

view this post on Zulip Bryan Gin-ge Chen (Jul 10 2020 at 04:26):

@Devon Tuma Done!

view this post on Zulip Scott Morrison (Jul 10 2020 at 04:26):

(I'd just found the page, and found a pending invite. :-) :racecar:

view this post on Zulip Devon Tuma (Jul 10 2020 at 04:40):

@Bryan Gin-ge Chen I didn't receive a github notification and still can't push a branch. Any idea what the problem might be?

view this post on Zulip Bryan Gin-ge Chen (Jul 10 2020 at 04:42):

Try this link? https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Devon Tuma (Jul 10 2020 at 04:42):

Yep that worked, thanks :+1:

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 14:05):

You get an email not a notification FWIW


Last updated: May 14 2021 at 23:14 UTC