Theorem polynomial.eval_eq_finset_sum'

chore(data/polynomial/*): delete, rename and move lemmas (#12852) …

feat(*): localized `R[X]` notation for `polynomial R` (#11895) …

feat(analysis): prove that a polynomial function is equivalent to its leading term along at_top, and consequences (#5354) …