## Stream: general

### Topic: Splitting data/polynomial

#### Aaron Anderson (Jul 15 2020 at 00:12):

@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 (Jul 15 2020 at 00:13):

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

#### Scott Morrison (Jul 15 2020 at 00:46):

Personally I think _everything_ should be in algebra/.

#### Johan Commelin (Jul 15 2020 at 04:04):

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

Last updated: May 15 2021 at 00:39 UTC