Commit 2025-10-25 18:20 985bd66b
View on Github →feat(RingTheory): Noetherian ring of fractions is semilocal (#30837)
A step towards showing invertible modules over Noetherian (comm.) rings are isomorphic to ideals, see https://mathoverflow.net/a/499611.
The argument is due to Gemini even though it was initially mistaken.
A ring of fractions is a ring R that is its own ring of fractions (i.e. satisfying IsFractionRing R R). We show this is equivalent to the condition that all non-zerodivisors are units.