Commit 2021-06-24 12:48 2a1cabea

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.