Stream: new members
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.
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.
Jalex Stark (Jul 09 2020 at 01:43):
you can read this guide to see what the process is like
Scott Morrison (Jul 09 2020 at 03:20):
Yes, these certainly belong in mathlib!
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.
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.
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
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.
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'
Bryan Gin-ge Chen (Jul 10 2020 at 04:26):
@Devon Tuma Done!
Scott Morrison (Jul 10 2020 at 04:26):
(I'd just found the page, and found a pending invite. :-) :racecar:
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?
Bryan Gin-ge Chen (Jul 10 2020 at 04:42):
Try this link? https://github.com/leanprover-community/mathlib/invitations
Devon Tuma (Jul 10 2020 at 04:42):
Yep that worked, thanks :+1:
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