mathlib

d8dd620c - feat(data/polynomial): a couple of lemmas on nat degree and roots of maps (#16992)

feat(data/polynomial): a couple of lemmas on nat degree and roots of maps (#16992) The nat_degree of sub lemmas complete the (nat/degree)-(add/sub) square. And the map lemma similar to those above lets the user provide injectivity of the map to avoid proving the image is non-zero which is often more convenient.