Commit 2021-06-10 01:51 06200c84

feat(ring_theory/ideal): generalize to noncommutative rings (#7654) This is a minimalist generalization of existing material on ideals to the setting of noncommutative rings. I have not attempted to decide how things should be named in the long run. For now ideal specifically means a left-ideal (i.e. I didn't change the definition). We can either in future add two_sided_ideal (or biideal or ideal₂ or ...), or potentially rename ideal to left_ideal or lideal, etc. Future bikeshedding opportunities! In this PR I've just left definitions alone, and relaxed comm_ring hypotheses to ring as far as I could see possible. No new theorems or mathematics, just rearranging to get things in the right order. (As a side note, both ring_theory.ideal.basic and ring_theory.ideal.operations should be split into smaller files; I can try this after this PR.)