mathlib3
e1c0b0a9 - feat(ring_theory/jacobson): Integral extension of Jacobson rings are Jacobson (#4304)

Commit

5 years ago

feat(ring_theory/jacobson): Integral extension of Jacobson rings are Jacobson (#4304) Main statement given by `is_jacobson_of_is_integral `

References

Author

dtumad

Parents