mathlib3

da32780c - chore(data/polynomial/*): create file `data/polynomial/inductions` and move around lemmas (#8563)

chore(data/polynomial/*): create file `data/polynomial/inductions` and move around lemmas (#8563) This PR is a precursor to #8463: it performs the move, without introducing lemmas and squeezes some `simp`s to make some proofs faster. I added add a doc-string to `lemma degree_pos_induction_on` with a reference to a lemma that will appear in #8463. The main reason why there are more added lines than removed ones is that the creation of a new file has a copyright statement, a module documentation and a few variable declarations.