Commit 2022-11-28 23:10 a00186d7
View on Github →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
.
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
.