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>

Author: kim-em

src/algebra/category/Module/projective.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison
 -/
-import category_theory.abelian.projective
+import category_theory.preadditive.projective
 import algebra.category.Module.abelian
 import linear_algebra.finsupp_vector_space
 import algebra.module.projective

src/algebra/group/units.lean

@@ -245,9 +245,17 @@ theorem is_unit_one [monoid M] : is_unit (1:M) := ⟨1, rfl⟩
   (a b : M) (h : a * b = 1) : is_unit a :=
 ⟨units.mk_of_mul_eq_one a b h, rfl⟩
 
+@[to_additive is_add_unit.exists_neg] theorem is_unit.exists_right_inv [monoid M]
+  {a : M} (h : is_unit a) : ∃ b, a * b = 1 :=
+by { rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩, exact ⟨b, hab⟩ }
+
+@[to_additive is_add_unit.exists_neg'] theorem is_unit.exists_left_inv [monoid M]
+  {a : M} (h : is_unit a) : ∃ b, b * a = 1 :=
+by { rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩, exact ⟨b, hba⟩ }
+
 @[to_additive is_add_unit_iff_exists_neg] theorem is_unit_iff_exists_inv [comm_monoid M]
   {a : M} : is_unit a ↔ ∃ b, a * b = 1 :=
-⟨by rintro ⟨⟨a, b, hab, _⟩, rfl⟩; exact ⟨b, hab⟩,
+⟨λ h, h.exists_right_inv,
  λ ⟨b, hab⟩, is_unit_of_mul_eq_one _ b hab⟩
 
 @[to_additive is_add_unit_iff_exists_neg'] theorem is_unit_iff_exists_inv' [comm_monoid M]