mathlib3

af7ba87a - feat(data/polynomial/eval): eval₂ f x (p * X) = eval₂ f x p * x (#5110)

feat(data/polynomial/eval): eval₂ f x (p * X) = eval₂ f x p * x (#5110) Also generalize `polynomial.eval₂_mul_noncomm` and `polynomial.eval₂_list_prod_noncomm`. This PR uses `add_monoid_algebra.lift_nc` to golf some proofs about `eval₂`. I'm not ready to replace the definition of `eval₂` yet (e.g., because it breaks dot notation everywhere), so I added a lemma `eval₂_eq_lift_nc` instead.