refactor(data/polynomial/eval): Golf `hom_eval₂` (#10920)
refactor(data/polynomial/eval): Golf `hom_eval₂` (#10920)

Here's a much easier proof of `hom_eval₂`.





leanprover-community/mathlib,leanprover-community/mathlib