mathlib

70e784d0 - feat(data/polynomial/*): `(p * q).trailing_degree = p.trailing_degree + q.trailing_degree` (#14384)

feat(data/polynomial/*): `(p * q).trailing_degree = p.trailing_degree + q.trailing_degree` (#14384) We already had a `nat_trailing_degree_mul` lemma, but this PR does things properly, following the analogous results for `degree`. In particular, we now have some useful intermediate results that do not assume `no_zero_divisors`.