Commit 2022-03-01 14:22 5a56e464
View on Github →chore(data/polynomial/monic): remove useless lemma (#12364)
There is a nontrivial version of this lemma (ne_zero_of_monic) which actually has uses in the library, unlike this deleted lemma. We also tidy the proof of the lemma below.