Commit 2022-08-09 17:00 d4b56199

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.