feat(data/polynomial): more API for roots (#11081)
`leading_coeff_monic_mul`
`leading_coeff_X_sub_C`
`root_multiplicity_C`
`not_is_root_C`
`roots_smul_nonzero`
`leading_coeff_div_by_monic_X_sub_C`
`roots_eq_zero_iff`
also generalized various statements about `X - C a` to `X + C a` over semirings.
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
