Commit 2021-10-05 03:31 15364121

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.