Division of MvPolynomial by monomials

Main definitions

• MvPolynomial.divMonomial x s: divides x by the monomial MvPolynomial.monomial 1 s
• MvPolynomial.modMonomial x s: the remainder upon dividing x by the monomial MvPolynomial.monomial 1 s.

Main results

• MvPolynomial.divMonomial_add_modMonomial, MvPolynomial.modMonomial_add_divMonomial: divMonomial and modMonomial are well-behaved as quotient and remainder operators.

Implementation notes

Where possible, the results in this file should be first proved in the generality of AddMonoidAlgebra, and then the versions specialized to MvPolynomial proved in terms of these.

Please ensure the declarations in this section are direct translations of AddMonoidAlgebra results.

noncomputable def MvPolynomial.divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial σ R

Divide by monomial 1 s, discarding terms not divisible by this.

@[simp]

theorem MvPolynomial.coeff_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R) (s' : σ →₀ ℕ) : MvPolynomial.coeff s' (MvPolynomial.divMonomial x s) = MvPolynomial.coeff (s + s') x

@[simp]

theorem MvPolynomial.support_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R) : MvPolynomial.support (MvPolynomial.divMonomial x s) = Finset.preimage (MvPolynomial.support x) ((fun x x_1 => x + x_1) s) (_ : Set.InjOn ((fun x x_1 => x + x_1) s) ((fun x x_1 => x + x_1) s ⁻¹' ↑(MvPolynomial.support x)))

@[simp]

theorem MvPolynomial.zero_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ℕ) : MvPolynomial.divMonomial 0 s = 0

theorem MvPolynomial.divMonomial_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) : MvPolynomial.divMonomial x 0 = x

theorem MvPolynomial.add_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (y : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial.divMonomial (x + y) s = MvPolynomial.divMonomial x s + MvPolynomial.divMonomial y s

theorem MvPolynomial.divMonomial_add {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ℕ) (b : σ →₀ ℕ) (x : MvPolynomial σ R) : MvPolynomial.divMonomial x (a + b) = MvPolynomial.divMonomial (MvPolynomial.divMonomial x a) b

@[simp]

theorem MvPolynomial.divMonomial_monomial_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ℕ) (x : MvPolynomial σ R) : MvPolynomial.divMonomial (↑(MvPolynomial.monomial a) 1 * x) a = x

@[simp]

theorem MvPolynomial.divMonomial_mul_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ℕ) (x : MvPolynomial σ R) : MvPolynomial.divMonomial (x * ↑(MvPolynomial.monomial a) 1) a = x

@[simp]

theorem MvPolynomial.divMonomial_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ℕ) : MvPolynomial.divMonomial (↑(MvPolynomial.monomial a) 1) a = 1

noncomputable def MvPolynomial.modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial σ R

The remainder upon division by monomial 1 s.

@[simp]

theorem MvPolynomial.coeff_modMonomial_of_not_le {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s' : σ →₀ ℕ} {s : σ →₀ ℕ} (x : MvPolynomial σ R) (h : ¬s ≤ s') : MvPolynomial.coeff s' (MvPolynomial.modMonomial x s) = MvPolynomial.coeff s' x

@[simp]

theorem MvPolynomial.coeff_modMonomial_of_le {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s' : σ →₀ ℕ} {s : σ →₀ ℕ} (x : MvPolynomial σ R) (h : s ≤ s') : MvPolynomial.coeff s' (MvPolynomial.modMonomial x s) = 0

@[simp]

theorem MvPolynomial.monomial_mul_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R) : MvPolynomial.modMonomial (↑(MvPolynomial.monomial s) 1 * x) s = 0

@[simp]

theorem MvPolynomial.mul_monomial_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R) : MvPolynomial.modMonomial (x * ↑(MvPolynomial.monomial s) 1) s = 0

@[simp]

theorem MvPolynomial.monomial_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ℕ) : MvPolynomial.modMonomial (↑(MvPolynomial.monomial s) 1) s = 0

theorem MvPolynomial.divMonomial_add_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ℕ) : ↑(MvPolynomial.monomial s) 1 * MvPolynomial.divMonomial x s + MvPolynomial.modMonomial x s = x

theorem MvPolynomial.modMonomial_add_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial.modMonomial x s + ↑(MvPolynomial.monomial s) 1 * MvPolynomial.divMonomial x s = x

theorem MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ →₀ ℕ} {x : MvPolynomial σ R} : ↑(MvPolynomial.monomial i) 1 ∣ x ↔ MvPolynomial.modMonomial x i = 0

@[simp]

theorem MvPolynomial.X_mul_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) (x : MvPolynomial σ R) : (MvPolynomial.divMonomial (MvPolynomial.X i * x) fun₀ | i => 1) = x

@[simp]

theorem MvPolynomial.X_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) : (MvPolynomial.divMonomial (MvPolynomial.X i) fun₀ | i => 1) = 1

@[simp]

theorem MvPolynomial.mul_X_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (i : σ) : (MvPolynomial.divMonomial (x * MvPolynomial.X i) fun₀ | i => 1) = x

@[simp]

theorem MvPolynomial.X_mul_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) (x : MvPolynomial σ R) : (MvPolynomial.modMonomial (MvPolynomial.X i * x) fun₀ | i => 1) = 0

@[simp]

theorem MvPolynomial.mul_X_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (i : σ) : (MvPolynomial.modMonomial (x * MvPolynomial.X i) fun₀ | i => 1) = 0

@[simp]

theorem MvPolynomial.modMonomial_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) : (MvPolynomial.modMonomial (MvPolynomial.X i) fun₀ | i => 1) = 0

theorem MvPolynomial.divMonomial_add_modMonomial_single {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (i : σ) : ((MvPolynomial.X i * MvPolynomial.divMonomial x fun₀ | i => 1) + MvPolynomial.modMonomial x fun₀ | i => 1) = x

theorem MvPolynomial.modMonomial_add_divMonomial_single {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (i : σ) : ((MvPolynomial.modMonomial x fun₀ | i => 1) + MvPolynomial.X i * MvPolynomial.divMonomial x fun₀ | i => 1) = x

theorem MvPolynomial.X_dvd_iff_modMonomial_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} {x : MvPolynomial σ R} : MvPolynomial.X i ∣ x ↔ (MvPolynomial.modMonomial x fun₀ | i => 1) = 0

Some results about dvd (∣) on monomial and X

theorem MvPolynomial.monomial_dvd_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] {r : R} {s : R} {i : σ →₀ ℕ} {j : σ →₀ ℕ} : ↑(MvPolynomial.monomial i) r ∣ ↑(MvPolynomial.monomial j) s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s

@[simp]

theorem MvPolynomial.monomial_one_dvd_monomial_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nontrivial R] {i : σ →₀ ℕ} {j : σ →₀ ℕ} : ↑(MvPolynomial.monomial i) 1 ∣ ↑(MvPolynomial.monomial j) 1 ↔ i ≤ j

@[simp]

theorem MvPolynomial.X_dvd_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nontrivial R] {i : σ} {j : σ} : MvPolynomial.X i ∣ MvPolynomial.X j ↔ i = j

@[simp]

theorem MvPolynomial.X_dvd_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} {j : σ →₀ ℕ} {r : R} : MvPolynomial.X i ∣ ↑(MvPolynomial.monomial j) r ↔ r = 0 ∨ ↑j i ≠ 0