feat(data/polynomial/monic): add two lemmas on degrees of monic polyn…

…omials (#11259)

This PR is a step in the direction of simplifying #11139.

The two lemmas involve computing the degree of a power of monic polynomials.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311139.20taylor.20sum.20and.20nat_degree_taylor)

src/data/polynomial/monic.lean

@@ -179,8 +179,21 @@ begin
   rw [← hndeg, ← polynomial.leading_coeff, hp.leading_coeff, C.map_one]
 end
 
+lemma nat_degree_pow (hp : p.monic) (n : ℕ) :
+  (p ^ n).nat_degree = n * p.nat_degree :=
+begin
+  induction n with n hn,
+  { simp },
+  { rw [pow_succ, hp.nat_degree_mul (monic_pow hp n), hn],
+    ring }
+end
+
 end monic
 
+@[simp] lemma nat_degree_pow_X_add_C [nontrivial R] (n : ℕ) (r : R) :
+  ((X + C r) ^ n).nat_degree = n :=
+by rw [(monic_X_add_C r).nat_degree_pow, nat_degree_X_add_C, mul_one]
+
 end semiring
 
 section comm_semiring