mathlib3

61d8b824 - chore(ring_theory/polynomial/quotient): remove spurious restrict_scalars (#18916)

chore(ring_theory/polynomial/quotient): remove spurious restrict_scalars (#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>