mathlib3

5a56e464 - chore(data/polynomial/monic): remove useless lemma (#12364)

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.