feat(FieldTheory/IsAlgClosed/Basic): generalize exists_aeval_eq_zero (#31311)

from `CommRing`+`IsSimpleRing` to `CommSemiring`+`FaithfulSMul`.

`Mathlib.Algebra.Algebra.IsSimpleRing` contains an instance of `FaithfulSMul` given `IsSimpleRing` if needed.

Author: SnirBroshi

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -181,9 +181,9 @@ theorem exists_aeval_eq_zero_of_injective {R : Type*} [CommSemiring R] [IsAlgClo
     ∃ x : k, aeval x p = 0 :=
   exists_eval₂_eq_zero_of_injective (algebraMap R k) hinj p hp
 
-theorem exists_aeval_eq_zero {R : Type*} [CommRing R] [IsSimpleRing R] [IsAlgClosed k] [Algebra R k]
-    (p : R[X]) (hp : p.degree ≠ 0) : ∃ x : k, p.aeval x = 0 :=
-  exists_eval₂_eq_zero _ _ hp
+theorem exists_aeval_eq_zero {R : Type*} [CommSemiring R] [IsAlgClosed k] [Algebra R k]
+    [FaithfulSMul R k] (p : R[X]) (hp : p.degree ≠ 0) : ∃ x : k, p.aeval x = 0 :=
+  exists_aeval_eq_zero_of_injective _ (FaithfulSMul.algebraMap_injective ..) _ hp
 
 
 /--

Mathlib/FieldTheory/IsSepClosed.lean

@@ -171,9 +171,10 @@ theorem exists_eval₂_eq_zero {k : Type*} [CommRing k] [IsSimpleRing k] [IsSepC
 
 variable (K)
 
-theorem exists_aeval_eq_zero {k : Type*} [CommRing k] [IsSimpleRing k] [IsSepClosed K] [Algebra k K]
-    (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x : K, p.aeval x = 0 :=
-  exists_eval₂_eq_zero _ _ hp hsep
+theorem exists_aeval_eq_zero {k : Type*} [CommSemiring k] [IsSepClosed K] [Algebra k K]
+    [FaithfulSMul k K] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
+    ∃ x : K, p.aeval x = 0 :=
+  exists_eval₂_eq_zero_of_injective _ (FaithfulSMul.algebraMap_injective ..) p hp hsep
 
 variable (k) {K}