mathlib

2a1cabea - chore(data/polynomial/eval, ring_theory/polynomial_algebra): golfs (#8058)

chore(data/polynomial/eval, ring_theory/polynomial_algebra): golfs (#8058) This golfs: * `polynomial.map_nat_cast` to use `ring_hom.map_nat_cast` * `polynomial.map.is_semiring_hom` to use `ring_hom.is_semiring_hom` * `poly_equiv_tensor.to_fun` and `poly_equiv_tensor.to_fun_linear_right` out of existence And adds a new (unused) lemma `polynomial.map_smul`. All the other changes in `polynomial/eval` are just reorderings of lemmas to allow the golfing.