mathlib

7d4f7730 - feat(ring_theory/jacobson): Proof that if a ring is a Jacobson Ring then so is its localization at a single element (#3651)

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. Co-authored-by: Devon Tuma <dtumad@gmail.com>