mathlib

06200c84 - feat(ring_theory/ideal): generalize to noncommutative rings (#7654)

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.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>