mathlib

9b779f40 - refactor(ring_theory/ideal/*, ring_theory/jacobson): use `comm_semiring` instead of `comm_ring` for ideals (#5954)

refactor(ring_theory/ideal/*, ring_theory/jacobson): use `comm_semiring` instead of `comm_ring` for ideals (#5954) This is the second pass at refactoring the definition of `ideal`. I have changed a `comm_ring` assumption to a `comm_semiring` assumption on many of the lemmas in `ring_theory/ideal/basic`. Most implied changes were very simple, with the usual exception of `jacobson`. I also moved out of `jacobson` the lemmas that were left-over from the previous refactor in this sequence. Besides changing such assumptions on other files, many of the lemmas in `ring_theory/ideal/basic` still using `comm_ring` and without explicit subtractions, deal with quotients.