chore(ring_theory/polynomial/quotient): remove spurious restrict_scal…

…ars (#18916)

Verifying that the `restrict_scalars` here is spurious. This proof is timing out badly in mathlib4.

If someone would like to merge this, please do so, but please then handle updating the SHA in mathlib4 as well. :-)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/ring_theory/polynomial/quotient.lean

@@ -22,7 +22,7 @@ variables {R : Type*} [comm_ring R]
 isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$. -/
 noncomputable def quotient_span_X_sub_C_alg_equiv (x : R) :
   (R[X] ⧸ ideal.span ({X - C x} : set R[X])) ≃ₐ[R] R :=
-(alg_equiv.restrict_scalars R $ ideal.quotient_equiv_alg_of_eq R
+(ideal.quotient_equiv_alg_of_eq R
   (by exact ker_eval_ring_hom x : ring_hom.ker (aeval x).to_ring_hom = _)).symm.trans $
   ideal.quotient_ker_alg_equiv_of_right_inverse $ λ _, eval_C