Multivariate polynomials over integral domains

This file proves results about multivariate polynomials that hold when the coefficient (semi)ring has no zero divisors.

theorem MvPolynomial.degreeOf_mul_eq {R : Type u_1} {σ : Type u_2} {n : σ} [CommSemiring R] {p q : MvPolynomial σ R} [NoZeroDivisors R] (hp : p ≠ 0) (hq : q ≠ 0) : degreeOf n (p * q) = degreeOf n p + degreeOf n q

theorem MvPolynomial.degreeOf_prod_eq {R : Type u_1} {σ : Type u_2} {n : σ} [CommSemiring R] [NoZeroDivisors R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R) (h : ∀ i ∈ s, f i ≠ 0) : degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

theorem MvPolynomial.degreeOf_pow_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] (i : σ) (p : MvPolynomial σ R) (n : ℕ) (hp : p ≠ 0) : degreeOf i (p ^ n) = n * degreeOf i p

theorem MvPolynomial.degrees_mul_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p q : MvPolynomial σ R} [NoZeroDivisors R] (hp : p ≠ 0) (hq : q ≠ 0) : (p * q).degrees = p.degrees + q.degrees

theorem MvPolynomial.totalDegree_mul_of_isDomain {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) : (f * g).totalDegree = f.totalDegree + g.totalDegree

theorem MvPolynomial.totalDegree_le_of_dvd_of_isDomain {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] {f g : MvPolynomial σ R} (h : f ∣ g) (hg : g ≠ 0) : f.totalDegree ≤ g.totalDegree

theorem MvPolynomial.dvd_C_iff_exists {R : Type u_1} {σ : Type u_2} [CommSemiring R] [NoZeroDivisors R] {f : MvPolynomial σ R} {a : R} (ha : a ≠ 0) : f ∣ C a ↔ ∃ (b : R), b ∣ a ∧ f = C b

theorem MvPolynomial.degreeOf_C_mul {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (j : σ) (c : R) (hc : c ∈ nonZeroDivisors R) : degreeOf j (C c * p) = degreeOf j p

theorem MvPolynomial.dvd_monomial_iff_exists {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {n : σ →₀ ℕ} {a : R} (ha : a ≠ 0) : p ∣ (monomial n) a ↔ ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

theorem MvPolynomial.dvd_monomial_one_iff_exists {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {n : σ →₀ ℕ} : p ∣ (monomial n) 1 ↔ ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m) u

theorem MvPolynomial.dvd_smul_X_iff_exists {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {i : σ} {r : R} (hr : r ≠ 0) : p ∣ r • X i ↔ ∃ (s : R), s ∣ r ∧ (p = C s ∨ p = s • X i)

theorem MvPolynomial.dvd_X_iff_exists {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {i : σ} : p ∣ X i ↔ ∃ (r : R), IsUnit r ∧ (p = C r ∨ p = r • X i)