feat(data/*): lemmas on division of polynomials by constant polynomia…

…ls (#4206)

From the Witt vector project
We provide a specialized version for polynomials over zmod n,
which turns out to be convenient in practice.


Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com>

src/data/mv_polynomial/basic.lean

@@ -442,6 +442,24 @@ lemma exists_coeff_ne_zero {p : mv_polynomial σ R} (h : p ≠ 0) :
   ∃ d, coeff d p ≠ 0 :=
 ne_zero_iff.mp h
 
+lemma C_dvd_iff_dvd_coeff (r : R) (φ : mv_polynomial σ R) :
+  C r ∣ φ ↔ ∀ i, r ∣ φ.coeff i :=
+begin
+  split,
+  { rintros ⟨φ, rfl⟩ c, rw coeff_C_mul, apply dvd_mul_right },
+  { intro h,
+    choose c hc using h,
+    classical,
+    let c' : (σ →₀ ℕ) → R := λ i, if i ∈ φ.support then c i else 0,
+    let ψ : mv_polynomial σ R := ∑ i in φ.support, monomial i (c' i),
+    use ψ,
+    apply mv_polynomial.ext, intro i,
+    simp only [coeff_C_mul, coeff_sum, coeff_monomial, finset.sum_ite_eq', c'],
+    split_ifs with hi hi,
+    { rw hc },
+    { rw finsupp.not_mem_support_iff at hi, rwa mul_zero } },
+end
+
 end coeff
 
 section constant_coeff
@@ -812,6 +830,15 @@ begin
   exact hf hx
 end
 
+lemma C_dvd_iff_map_hom_eq_zero
+  (q : R →+* S₁) (r : R) (hr : ∀ r' : R, q r' = 0 ↔ r ∣ r')
+  (φ : mv_polynomial σ R) :
+  C r ∣ φ ↔ map q φ = 0 :=
+begin
+  rw [C_dvd_iff_dvd_coeff, mv_polynomial.ext_iff],
+  simp only [coeff_map, ring_hom.coe_of, coeff_zero, hr],
+end
+
 end map
 
 

src/data/zmod/polynomial.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import data.mv_polynomial.basic
+import data.zmod.basic
+
+/-!
+## Facts concerning polynomials over `zmod n`
+-/
+
+namespace mv_polynomial
+
+/-- A polynomial over the integers is divisible by `n : ℕ`
+if and only if it is zero over `zmod n`. -/
+lemma C_dvd_iff_zmod {σ : Type*} (n : ℕ) (φ : mv_polynomial σ ℤ) :
+  C (n:ℤ) ∣ φ ↔ map (int.cast_ring_hom (zmod n)) φ = 0 :=
+C_dvd_iff_map_hom_eq_zero _ _ (char_p.int_cast_eq_zero_iff (zmod n) n) _
+
+end mv_polynomial