chore(Algebra/FieldTheory/IsAlgClosed/Basic): ungeneralize exists_aeval_eq_zero from CommSemiring + FaithfulSMul to CommRing + IsSimpleRing

For `FaithfulSMul` to be a generalization we need to import `Mathlib.Algebra.Algebra.IsSimpleRing` which contains an instance of `FaithfulSMul` given `IsSimpleRing`

Author: SnirBroshi

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -175,11 +175,11 @@ variable (k)
 theorem exists_aeval_eq_zero_of_injective {R : Type*} [CommSemiring R] [IsAlgClosed k] [Algebra R k]
     (hinj : Function.Injective (algebraMap R k)) (p : R[X]) (hp : p.degree ≠ 0) :
     ∃ x : k, aeval x p = 0 :=
-  exists_eval₂_eq_zero_of_injective _ hinj _ hp
+  exists_eval₂_eq_zero_of_injective (algebraMap R k) hinj p 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, aeval x p = 0 :=
-  exists_aeval_eq_zero_of_injective _ (FaithfulSMul.algebraMap_injective _ _) _ 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
 
 
 /--

Mathlib/FieldTheory/IsSepClosed.lean

@@ -167,10 +167,9 @@ theorem exists_eval₂_eq_zero {k : Type*} [CommRing k] [IsSimpleRing k] [IsSepC
 
 variable (K)
 
-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
+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
 
 variable (k) {K}