chore: generalised some results from ring to semiring (#8715)

Changed the hypothesis of some results from ring to semiring, without changing the proofs. 



Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>

Mathlib/RingTheory/Ideal/Basic.lean

@@ -276,7 +276,7 @@ theorem zero_ne_one_of_proper {I : Ideal α} (h : I ≠ ⊤) : (0 : α) ≠ 1 :=
   I.ne_top_iff_one.1 h <| hz ▸ I.zero_mem
 #align ideal.zero_ne_one_of_proper Ideal.zero_ne_one_of_proper
 
-theorem bot_prime {R : Type*} [Ring R] [IsDomain R] : (⊥ : Ideal R).IsPrime :=
+theorem bot_prime [IsDomain α] : (⊥ : Ideal α).IsPrime :=
   ⟨fun h => one_ne_zero (by rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h), fun h =>
     mul_eq_zero.mp (by simpa only [Submodule.mem_bot] using h)⟩
 #align ideal.bot_prime Ideal.bot_prime
@@ -347,8 +347,8 @@ instance [Nontrivial α] : Nontrivial (Ideal α) := by
 
 /-- If P is not properly contained in any maximal ideal then it is not properly contained
   in any proper ideal -/
-theorem maximal_of_no_maximal {R : Type u} [Semiring R] {P : Ideal R}
-    (hmax : ∀ m : Ideal R, P < m → ¬IsMaximal m) (J : Ideal R) (hPJ : P < J) : J = ⊤ := by
+theorem maximal_of_no_maximal {P : Ideal α}
+    (hmax : ∀ m : Ideal α, P < m → ¬IsMaximal m) (J : Ideal α) (hPJ : P < J) : J = ⊤ := by
   by_contra hnonmax
   rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩
   exact hmax M (lt_of_lt_of_le hPJ hM2) hM1
@@ -542,14 +542,14 @@ instance (priority := 100) IsMaximal.isPrime' (I : Ideal α) : ∀ [_H : I.IsMax
   @IsMaximal.isPrime _ _ _
 #align ideal.is_maximal.is_prime' Ideal.IsMaximal.isPrime'
 
-theorem span_singleton_lt_span_singleton [CommRing β] [IsDomain β] {x y : β} :
-    span ({x} : Set β) < span ({y} : Set β) ↔ DvdNotUnit y x := by
+theorem span_singleton_lt_span_singleton [IsDomain α] {x y : α} :
+    span ({x} : Set α) < span ({y} : Set α) ↔ DvdNotUnit y x := by
   rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
     dvd_and_not_dvd_iff]
 #align ideal.span_singleton_lt_span_singleton Ideal.span_singleton_lt_span_singleton
 
-theorem factors_decreasing [CommRing β] [IsDomain β] (b₁ b₂ : β) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) :
-    span ({b₁ * b₂} : Set β) < span {b₁} :=
+theorem factors_decreasing [IsDomain α] (b₁ b₂ : α) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) :
+    span ({b₁ * b₂} : Set α) < span {b₁} :=
   lt_of_le_not_le
     (Ideal.span_le.2 <| singleton_subset_iff.2 <| Ideal.mem_span_singleton.2 ⟨b₂, rfl⟩) fun h =>
     h₂ <| isUnit_of_dvd_one <|
@@ -836,7 +836,7 @@ end Ring
 
 namespace Ideal
 
-variable {R : Type u} [CommRing R] [Nontrivial R]
+variable {R : Type u} [CommSemiring R] [Nontrivial R]
 
 theorem bot_lt_of_maximal (M : Ideal R) [hm : M.IsMaximal] (non_field : ¬IsField R) : ⊥ < M := by
   rcases Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top.1 non_field with ⟨I, Ibot, Itop⟩