feat(RingTheory/Ideal/Quotient): assume Semiring instance instead of …

…CommRing (#9493)

Ideal.Quotient.lift only needs `Semiring S` on the target to work.

This PR only changes one line : `variable [CommRing S]` to `variable [Semiring S]`



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>

Mathlib/RingTheory/Ideal/Quotient.lean

@@ -251,7 +251,7 @@ theorem maximal_ideal_iff_isField_quotient (I : Ideal R) : I.IsMaximal ↔ IsFie
     maximal_of_isField _⟩
 #align ideal.quotient.maximal_ideal_iff_is_field_quotient Ideal.Quotient.maximal_ideal_iff_isField_quotient
 
-variable [CommRing S]
+variable [Semiring S]
 
 /-- Given a ring homomorphism `f : R →+* S` sending all elements of an ideal to zero,
 lift it to the quotient by this ideal. -/