Reintroducing quotient rings in RingTheory.Polynomial.Basic

Stream: mathlib4

[Anatole Dedecker]

!3#18530 removed the dependency of RingTheory.Polynomial.Basic on quotient rings, in order to make the port go smoother. Is it fine to reintroduce such a dependency at this point? Judging by the discussion on that PR and the porting notes it looks like it was a temporary restriction anyways, since some of the proofs were uglified to make that work.
I'm asking this in the context of #4691, where @Emilie Uthaiwat adds her main result to RingTheory.Polynomial.Quotient just because it's the first file that has all of the neccessary import, but that feels wrong since this result is not at all about quotients of polynomial rings like the rest of the file.

[Riccardo Brasca]

I helped Emilie choosing the file (this is her first PR) and I confirm that the logic was just "let's try to not touch any import during the port".

[Riccardo Brasca]

I don't have a real opinion on !3#18530

[Anatole Dedecker]

@Johan Commelin @Scott Morrison Sorry to bother, could I get your opinion on this? I'm not suggesting undoing !3#18530 right now, this is about reintroducing the import but for new content?

[Johan Commelin]

I have no problem with undoing that split. It was motivated by the eta for structures problem. But since that is now gone, please go ahead and restructure files in a mathematically sensible way.