Zulip Chat Archive

Stream: general

Topic: Splitting data/polynomial


view this post on Zulip 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.

view this post on Zulip 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/?

view this post on Zulip Scott Morrison (Jul 15 2020 at 00:46):

Personally I think _everything_ should be in algebra/.

view this post on Zulip 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