Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-23 16:22 7d4f7730

View on Github →

feat(ring_theory/jacobson): Proof that if a ring is a Jacobson Ring then so is its localization at a single element (#3651) The main result here is that the localization of a Jacobson ring to a single element is also a Jacobson ring, which is one of the things needed for the proof that R is Jacobson if and only if R[x] is Jacobson. Two characterization of Jacobson rings in terms of their quotient rings are also included, again needed to prove R[x] is Jacobson.

Estimated changes