chore(data/polynomial/induction): cleanup (#15918)
Even ignoring the confusion with `data/polynomial/inductions.lean` (out of scope for this PR), this file is a bit of a mess:
* The coeff and summation lemmas are out of place
* Some lemmas use a weird `inverse` naming to refer to `set.preimage`.
* Some lemmas use `submodule.span` instead of `ideal.span`.
This PR moves, renames, and restates the lemmas above as necessary.
Some proofs have been golfed to enable the shuffling, but all lemma statements are defeq to the originals.
