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.

src/data/polynomial/degree/definitions.lean

@@ -1073,6 +1073,14 @@ by { rw ← degree_neg q at h, rw [sub_eq_add_neg, degree_add_eq_left_of_degree_
 lemma degree_sub_eq_right_of_degree_lt (h : degree p < degree q) : degree (p - q) = degree q :=
 by { rw ← degree_neg q at h, rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg] }
 
+lemma nat_degree_sub_eq_left_of_nat_degree_lt (h : nat_degree q < nat_degree p) :
+  nat_degree (p - q) = nat_degree p :=
+nat_degree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt (degree_lt_degree h))
+
+lemma nat_degree_sub_eq_right_of_nat_degree_lt (h : nat_degree p < nat_degree q) :
+  nat_degree (p - q) = nat_degree q :=
+nat_degree_eq_of_degree_eq (degree_sub_eq_right_of_degree_lt (degree_lt_degree h))
+
 end ring
 
 section nonzero_ring

src/data/polynomial/ring_division.lean

@@ -923,6 +923,13 @@ lemma card_roots_le_map [is_domain A] [is_domain B] {p : A[X]} {f : A →+* B} (
   p.roots.card ≤ (p.map f).roots.card :=
 by { rw ← p.roots.card_map f, exact multiset.card_le_of_le (map_roots_le h) }
 
+lemma card_roots_le_map_of_injective [is_domain A] [is_domain B] {p : A[X]} {f : A →+* B}
+  (hf : function.injective f) : p.roots.card ≤ (p.map f).roots.card :=
+begin
+  by_cases hp0 : p = 0, { simp only [hp0, roots_zero, polynomial.map_zero, multiset.card_zero], },
+  exact card_roots_le_map ((polynomial.map_ne_zero_iff hf).mpr hp0),
+end
+
 lemma roots_map_of_injective_of_card_eq_nat_degree [is_domain A] [is_domain B] {p : A[X]}
   {f : A →+* B} (hf : function.injective f) (hroots : p.roots.card = p.nat_degree) :
   p.roots.map f = (p.map f).roots :=