Commit 2021-02-01 22:55 9b779f40

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.