polynomial big_ops lemmas

Stream: general

[Jalex Stark]

In the branch mathlib:characteristic_polynomial_trace, @Aaron Anderson proves that the trace is a coefficient of the characteristic polynomial. We're trying to break it into smaller PRs. We have a section with some big_ops lemmas such as

lemma nat_degree_prod_le :
(s.prod f).nat_degree ≤ ∑ i in s, (f i).nat_degree

Where should they go? data/polynomial.lean seems bloated

[Anne Baanen]

There is a directory ring_theory/polynomial, which might be overly specific though.

[Anne Baanen]

It's more algebra than ring_theory to me.

[Jalex Stark]

does it make sense to have a file algebra/polynomial.lean?

[Jalex Stark]

things which could fit in data/polynomial.lean but aren't useful for programming can go to algebra/polynomial.lean instead

[Scott Morrison]

Yes. I think soon I would like to move data/polynomial.lean to algebra/polynomial/basic.lean, and then move half of its contents out into other files in that directory. It's far too big already.

[Scott Morrison]

I'm not going to do that immediately, so if anyone wants to make a start on putting new material in new files that would be great.

[Jalex Stark]

we have started on this in #3378