Is this worth contributing to mathlib?

Stream: new members

[Devon Tuma]

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.

[Jalex Stark]

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

[Jalex Stark]

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

[Scott Morrison]

Yes, these certainly belong in mathlib!

[Johan Commelin]

@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.

[Devon Tuma]

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.

[Devon Tuma]

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

[Yury G. Kudryashov]

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

[Devon Tuma]

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

[Bryan Gin-ge Chen]

@Devon Tuma Done!

[Scott Morrison]

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

[Devon Tuma]

@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?

[Bryan Gin-ge Chen]

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

[Devon Tuma]

Yep that worked, thanks :+1:

[Kevin Buzzard]

You get an email not a notification FWIW