definitions): Remove duplicate lemma (#17740)

Commit

3 years ago

refactor(data/polynomial/degree/definitions): Remove duplicate lemma (#17740) This PR golfs `zero_le_degree_iff`, and removes the redundant lemma `degree_nonneg_iff_ne_zero`.

Author

tb65536

Parents

f2f23df7

mathlib3 a00186d7 - refactor(data/polynomial/degree/definitions): Remove duplicate lemma (#17740)

mathlib3
a00186d7 - refactor(data/polynomial/degree/definitions): Remove duplicate lemma (#17740)