refactor(ring_theory/*): Remove unnecessary commutativity assumptions (…

…#13966)

This replaces `[comm_ring R]` or `[comm_semiring R]` with `[ring R]` or `[semiring R]`, without changing any proofs.

src/ring_theory/artinian.lean

@@ -373,20 +373,20 @@ theorem is_artinian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module R
   [is_artinian_ring R] {A : set M} (hA : finite A) : is_artinian R (submodule.span R A) :=
 is_artinian_of_fg_of_artinian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)
 
-theorem is_artinian_ring_of_surjective (R) [comm_ring R] (S) [comm_ring S]
+theorem is_artinian_ring_of_surjective (R) [ring R] (S) [ring S]
   (f : R →+* S) (hf : function.surjective f)
   [H : is_artinian_ring R] : is_artinian_ring S :=
 begin
   rw [is_artinian_ring_iff, is_artinian_iff_well_founded] at H ⊢,
   exact order_embedding.well_founded (ideal.order_embedding_of_surjective f hf) H,
 end
 
-instance is_artinian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R →+* S)
+instance is_artinian_ring_range {R} [ring R] {S} [ring S] (f : R →+* S)
   [is_artinian_ring R] : is_artinian_ring f.range :=
 is_artinian_ring_of_surjective R f.range f.range_restrict
   f.range_restrict_surjective
 
-theorem is_artinian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
+theorem is_artinian_ring_of_ring_equiv (R) [ring R] {S} [ring S]
   (f : R ≃+* S) [is_artinian_ring R] : is_artinian_ring S :=
 is_artinian_ring_of_surjective R S f.to_ring_hom f.to_equiv.surjective
 

src/ring_theory/finiteness.lean

@@ -134,7 +134,7 @@ lemma trans {R : Type*} (A B : Type*) [comm_semiring R] [comm_semiring A] [algeb
       ht, submodule.restrict_scalars_top]⟩⟩
 
 @[priority 100] -- see Note [lower instance priority]
-instance finite_type {R : Type*} (A : Type*) [comm_semiring R] [comm_semiring A]
+instance finite_type {R : Type*} (A : Type*) [comm_semiring R] [semiring A]
   [algebra R A] [hRA : finite R A] : algebra.finite_type R A :=
 ⟨subalgebra.fg_of_submodule_fg hRA.1⟩
 

src/ring_theory/ideal/basic.lean

@@ -15,15 +15,16 @@ import linear_algebra.finsupp
 
 # Ideals over a ring
 
-This file defines `ideal R`, the type of ideals over a commutative ring `R`.
+This file defines `ideal R`, the type of (left) ideals over a ring `R`.
+Note that over commutative rings, left ideals and two-sided ideals are equivalent.
 
 ## Implementation notes
 
 `ideal R` is implemented using `submodule R R`, where `•` is interpreted as `*`.
 
 ## TODO
 
-Support one-sided ideals, and ideals over non-commutative rings.
+Support right ideals, and two-sided ideals over non-commutative rings.
 -/
 
 universes u v w
@@ -232,7 +233,7 @@ end
 
 /-- If P is not properly contained in any maximal ideal then it is not properly contained
   in any proper ideal -/
-lemma maximal_of_no_maximal {R : Type u} [comm_semiring R] {P : ideal R}
+lemma maximal_of_no_maximal {R : Type u} [semiring R] {P : ideal R}
 (hmax : ∀ m : ideal R, P < m → ¬is_maximal m) (J : ideal R) (hPJ : P < J) : J = ⊤ :=
 begin
   by_contradiction hnonmax,

src/ring_theory/noetherian.lean

@@ -288,7 +288,7 @@ begin
   { rwa [inf_of_le_right (show f.ker ≤ (comap f g.ker), from comap_mono bot_le)] }
 end
 
-lemma fg_restrict_scalars {R S M : Type*} [comm_ring R] [comm_ring S] [algebra R S]
+lemma fg_restrict_scalars {R S M : Type*} [comm_semiring R] [semiring S] [algebra R S]
   [add_comm_group M] [module S M] [module R M] [is_scalar_tower R S M] (N : submodule S M)
   (hfin : N.fg) (h : function.surjective (algebra_map R S)) : (submodule.restrict_scalars R N).fg :=
 begin
@@ -668,8 +668,8 @@ class is_noetherian_ring (R) [semiring R] extends is_noetherian R R : Prop
 theorem is_noetherian_ring_iff {R} [semiring R] : is_noetherian_ring R ↔ is_noetherian R R :=
 ⟨λ h, h.1, @is_noetherian_ring.mk _ _⟩
 
-/-- A commutative ring is Noetherian if and only if all its ideals are finitely-generated. -/
-lemma is_noetherian_ring_iff_ideal_fg (R : Type*) [comm_semiring R] :
+/-- A ring is Noetherian if and only if all its ideals are finitely-generated. -/
+lemma is_noetherian_ring_iff_ideal_fg (R : Type*) [semiring R] :
   is_noetherian_ring R ↔ ∀ I : ideal R, I.fg :=
 is_noetherian_ring_iff.trans is_noetherian_def
 
@@ -756,20 +756,20 @@ theorem is_noetherian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module
   [is_noetherian_ring R] {A : set M} (hA : finite A) : is_noetherian R (submodule.span R A) :=
 is_noetherian_of_fg_of_noetherian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)
 
-theorem is_noetherian_ring_of_surjective (R) [comm_ring R] (S) [comm_ring S]
+theorem is_noetherian_ring_of_surjective (R) [ring R] (S) [ring S]
   (f : R →+* S) (hf : function.surjective f)
   [H : is_noetherian_ring R] : is_noetherian_ring S :=
 begin
   rw [is_noetherian_ring_iff, is_noetherian_iff_well_founded] at H ⊢,
   exact order_embedding.well_founded (ideal.order_embedding_of_surjective f hf).dual H,
 end
 
-instance is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R →+* S)
+instance is_noetherian_ring_range {R} [ring R] {S} [ring S] (f : R →+* S)
   [is_noetherian_ring R] : is_noetherian_ring f.range :=
 is_noetherian_ring_of_surjective R f.range f.range_restrict
   f.range_restrict_surjective
 
-theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
+theorem is_noetherian_ring_of_ring_equiv (R) [ring R] {S} [ring S]
   (f : R ≃+* S) [is_noetherian_ring R] : is_noetherian_ring S :=
 is_noetherian_ring_of_surjective R S f.to_ring_hom f.to_equiv.surjective