Commit 2020-11-27 09:16 af7ba87a

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.