feat(polynomial): prepare for transcendence of e by adding small lemm…

…as (#4175)

This will be a series of pull request to prepare for the proof of transcendence of e by adding lots of small lemmas.




Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/polynomial/basic.lean

@@ -117,6 +117,14 @@ by rw [←one_smul R p, ←h, zero_smul]
 
 end semiring
 
+section comm_semiring
+variables [comm_semiring R]
+
+instance : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
+instance : comm_monoid (polynomial R) := comm_semiring.to_comm_monoid (polynomial R)
+
+end comm_semiring
+
 section ring
 variables [ring R]
 
@@ -129,7 +137,6 @@ lemma coeff_sub (p q : polynomial R) (n : ℕ) : coeff (p - q) n = coeff p n - c
 
 end ring
 
-instance [comm_semiring R] : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
 instance [comm_ring R] : comm_ring (polynomial R) := add_monoid_algebra.comm_ring
 
 section nonzero_semiring

src/data/polynomial/coeff.lean

@@ -42,6 +42,9 @@ coeff (r • p) n = r * coeff p n := finsupp.smul_apply
 lemma mem_support_iff_coeff_ne_zero : n ∈ p.support ↔ p.coeff n ≠ 0 :=
 by { rw mem_support_to_fun, refl }
 
+lemma not_mem_support_iff_coeff_zero : n ∉ p.support ↔ p.coeff n = 0 :=
+by { rw [mem_support_to_fun, not_not], refl, }
+
 variable (R)
 /-- The nth coefficient, as a linear map. -/
 def lcoeff (n : ℕ) : polynomial R →ₗ[R] R :=

src/data/polynomial/degree.lean

@@ -48,6 +48,18 @@ else with_bot.coe_le_coe.1 $
         (le_nat_degree_of_ne_zero (finsupp.mem_support_iff.1 hn))
         (nat.zero_le _))
 
+lemma eq_C_of_nat_degree_eq_zero (hp : p.nat_degree = 0) : p = C (p.coeff 0) :=
+begin
+  ext, induction n with n hn,
+  { simp only [polynomial.coeff_C_zero], },
+  { have ineq : p.nat_degree < n.succ := hp.symm ▸ n.succ_pos,
+    have zero1 : p.coeff n.succ = 0 := coeff_eq_zero_of_nat_degree_lt ineq,
+    have zero2 : (C (p.coeff 0)).nat_degree = 0 := nat_degree_C (p.coeff 0),
+    have zero3 : (C (p.coeff 0)).coeff n.succ = 0 :=
+      coeff_eq_zero_of_nat_degree_lt (zero2.symm ▸ n.succ_pos),
+    rw [zero1, zero3], }
+end
+
 lemma degree_map_le [semiring S] (f : R →+* S) :
   degree (p.map f) ≤ degree p :=
 if h : p.map f = 0 then by simp [h]

src/data/polynomial/derivative.lean

@@ -212,6 +212,26 @@ le_antisymm
     exact hp
   end
 
+theorem nat_degree_eq_zero_of_derivative_eq_zero [char_zero R] {f : polynomial R} (h : f.derivative = 0) :
+  f.nat_degree = 0 :=
+begin
+  by_cases hf : f = 0,
+  { exact (congr_arg polynomial.nat_degree hf).trans rfl },
+  { rw nat_degree_eq_zero_iff_degree_le_zero,
+    by_contra absurd,
+    have f_nat_degree_pos : 0 < f.nat_degree,
+    { rwa [not_le, ←nat_degree_pos_iff_degree_pos] at absurd },
+    let m := f.nat_degree - 1,
+    have hm : m + 1 = f.nat_degree := nat.sub_add_cancel f_nat_degree_pos,
+    have h2 := coeff_derivative f m,
+    rw polynomial.ext_iff at h,
+    rw [h m, coeff_zero, zero_eq_mul] at h2,
+    cases h2,
+    { rw [hm, ←leading_coeff, leading_coeff_eq_zero] at h2,
+      exact hf h2, },
+    { norm_cast at h2 } }
+end
+
 end domain
 
 end derivative