Splitting data/polynomial

Stream: general

[Aaron Anderson]

@Jalex Stark and I have started pushing some polynomial lemmas to algebra/polynomial/, because data/polynomial is disorientingly full. @Johan Commelin pointed out that we'll have a much easier time if we break up that file first, and then push our new lemmas.

[Aaron Anderson]

What opinions do people have on which definitions and lemmas about polynomials belong in data/, and which belong in algebra/?

[Scott Morrison]

Personally I think _everything_ should be in algebra/.

[Johan Commelin]

Since we made polynomials noncomputable some time ago, I think that it's safe to move them out of data/ entirely.