feat(data/polynomial): some lemmas about (nat)degree of bit0/1 in cha…

…r_zero (#15726)

src/data/polynomial/coeff.lean

@@ -36,6 +36,8 @@ coeff_monomial
 lemma coeff_add (p q : R[X]) (n : ℕ) : coeff (p + q) n = coeff p n + coeff q n :=
 by { rcases p, rcases q, simp_rw [←of_finsupp_add, coeff], exact finsupp.add_apply _ _ _ }
 
+@[simp] lemma coeff_bit0 (p : R[X]) (n : ℕ) : coeff (bit0 p) n = bit0 (coeff p n) := by simp [bit0]
+
 @[simp] lemma coeff_smul [monoid S] [distrib_mul_action S R] (r : S) (p : R[X]) (n : ℕ) :
   coeff (r • p) n = r • coeff p n :=
 by { rcases p, simp_rw [←of_finsupp_smul, coeff], exact finsupp.smul_apply _ _ _ }

src/data/polynomial/ring_division.lean

@@ -160,6 +160,36 @@ begin
   rw [← nat_degree_mul hp₁ hq₂, ← nat_degree_mul hp₂ hq₁, h_eq]
 end
 
+variables [char_zero R]
+
+@[simp] lemma degree_bit0_eq (p : R[X]) : degree (bit0 p) = degree p :=
+by rw [bit0_eq_two_mul, degree_mul, (by simp : (2 : polynomial R) = C 2),
+  @polynomial.degree_C R _ _ two_ne_zero', zero_add]
+
+@[simp] lemma nat_degree_bit0_eq (p : R[X]) : nat_degree (bit0 p) = nat_degree p :=
+nat_degree_eq_of_degree_eq $ degree_bit0_eq p
+
+@[simp]
+lemma nat_degree_bit1_eq (p : R[X]) : nat_degree (bit1 p) = nat_degree p :=
+begin
+  rw bit1,
+  apply le_antisymm,
+  convert nat_degree_add_le _ _,
+  { simp, },
+  by_cases h : p.nat_degree = 0,
+  { simp [h], },
+  apply le_nat_degree_of_ne_zero,
+  intro hh,
+  apply h,
+  simp [*, coeff_one, if_neg (ne.symm h)] at *,
+end
+
+lemma degree_bit1_eq {p : R[X]} (hp : 0 < degree p) : degree (bit1 p) = degree p :=
+begin
+  rw [bit1, degree_add_eq_left_of_degree_lt, degree_bit0_eq],
+  rwa [degree_one, degree_bit0_eq]
+end
+
 end no_zero_divisors
 
 section no_zero_divisors