mathlib3

15364121 - refactor(data/polynomial): use `monic.ne_zero` and `nontriviality` (#9530)

refactor(data/polynomial): use `monic.ne_zero` and `nontriviality` (#9530) There is a pattern in `data/polynomial` to have both `(hq : q.monic) (hq0 : q ≠ 0)` as assumptions. I found this less convenient to work with than `[nontrivial R] (hq : q.monic)` and using `monic.ne_zero` to replace `hq0`. The `nontriviality` tactic automates all the cases where previously `nontrivial R` (or similar) was manually derived from the hypotheses.