Division of mv_polynomial by monomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
mv_polynomial.div_monomial x s: dividesxby the monomialmv_polynomial.monomial 1 smv_polynomial.mod_monomial x s: the remainder upon dividingxby the monomialmv_polynomial.monomial 1 s.
Main results #
mv_polynomial.div_monomial_add_mod_monomial,mv_polynomial.mod_monomial_add_div_monomial:div_monomialandmod_monomialare well-behaved as quotient and remainder operators.
Implementation notes #
Where possible, the results in this file should be first proved in the generality of
add_monoid_algebra, and then the versions specialized to mv_polynomial proved in terms of these.
Please ensure the declarations in this section are direct translations of add_monoid_algebra
results.
noncomputable
def
mv_polynomial.div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(p : mv_polynomial σ R)
(s : σ →₀ ℕ) :
mv_polynomial σ R
Divide by monomial 1 s, discarding terms not divisible by this.
Equations
- p.div_monomial s = add_monoid_algebra.div_of p s
@[simp]
theorem
mv_polynomial.coeff_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(s : σ →₀ ℕ)
(x : mv_polynomial σ R)
(s' : σ →₀ ℕ) :
mv_polynomial.coeff s' (x.div_monomial s) = mv_polynomial.coeff (s + s') x
@[simp]
theorem
mv_polynomial.support_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(s : σ →₀ ℕ)
(x : mv_polynomial σ R) :
(x.div_monomial s).support = x.support.preimage (has_add.add s) _
@[simp]
theorem
mv_polynomial.zero_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(s : σ →₀ ℕ) :
0.div_monomial s = 0
theorem
mv_polynomial.div_monomial_zero
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R) :
x.div_monomial 0 = x
theorem
mv_polynomial.add_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x y : mv_polynomial σ R)
(s : σ →₀ ℕ) :
(x + y).div_monomial s = x.div_monomial s + y.div_monomial s
theorem
mv_polynomial.div_monomial_add
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(a b : σ →₀ ℕ)
(x : mv_polynomial σ R) :
x.div_monomial (a + b) = (x.div_monomial a).div_monomial b
@[simp]
theorem
mv_polynomial.div_monomial_monomial_mul
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(a : σ →₀ ℕ)
(x : mv_polynomial σ R) :
(⇑(mv_polynomial.monomial a) 1 * x).div_monomial a = x
@[simp]
theorem
mv_polynomial.div_monomial_mul_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(a : σ →₀ ℕ)
(x : mv_polynomial σ R) :
(x * ⇑(mv_polynomial.monomial a) 1).div_monomial a = x
@[simp]
theorem
mv_polynomial.div_monomial_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(a : σ →₀ ℕ) :
(⇑(mv_polynomial.monomial a) 1).div_monomial a = 1
noncomputable
def
mv_polynomial.mod_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R)
(s : σ →₀ ℕ) :
mv_polynomial σ R
The remainder upon division by monomial 1 s.
Equations
- x.mod_monomial s = add_monoid_algebra.mod_of x s
@[simp]
theorem
mv_polynomial.coeff_mod_monomial_of_not_le
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{s' s : σ →₀ ℕ}
(x : mv_polynomial σ R)
(h : ¬s ≤ s') :
mv_polynomial.coeff s' (x.mod_monomial s) = mv_polynomial.coeff s' x
@[simp]
theorem
mv_polynomial.coeff_mod_monomial_of_le
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{s' s : σ →₀ ℕ}
(x : mv_polynomial σ R)
(h : s ≤ s') :
mv_polynomial.coeff s' (x.mod_monomial s) = 0
@[simp]
theorem
mv_polynomial.monomial_mul_mod_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(s : σ →₀ ℕ)
(x : mv_polynomial σ R) :
(⇑(mv_polynomial.monomial s) 1 * x).mod_monomial s = 0
@[simp]
theorem
mv_polynomial.mul_monomial_mod_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(s : σ →₀ ℕ)
(x : mv_polynomial σ R) :
(x * ⇑(mv_polynomial.monomial s) 1).mod_monomial s = 0
@[simp]
theorem
mv_polynomial.monomial_mod_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(s : σ →₀ ℕ) :
(⇑(mv_polynomial.monomial s) 1).mod_monomial s = 0
theorem
mv_polynomial.div_monomial_add_mod_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R)
(s : σ →₀ ℕ) :
⇑(mv_polynomial.monomial s) 1 * x.div_monomial s + x.mod_monomial s = x
theorem
mv_polynomial.mod_monomial_add_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R)
(s : σ →₀ ℕ) :
x.mod_monomial s + ⇑(mv_polynomial.monomial s) 1 * x.div_monomial s = x
theorem
mv_polynomial.monomial_one_dvd_iff_mod_monomial_eq_zero
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{i : σ →₀ ℕ}
{x : mv_polynomial σ R} :
⇑(mv_polynomial.monomial i) 1 ∣ x ↔ x.mod_monomial i = 0
@[simp]
theorem
mv_polynomial.X_mul_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(i : σ)
(x : mv_polynomial σ R) :
(mv_polynomial.X i * x).div_monomial (finsupp.single i 1) = x
@[simp]
theorem
mv_polynomial.X_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(i : σ) :
(mv_polynomial.X i).div_monomial (finsupp.single i 1) = 1
@[simp]
theorem
mv_polynomial.mul_X_div_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R)
(i : σ) :
(x * mv_polynomial.X i).div_monomial (finsupp.single i 1) = x
@[simp]
theorem
mv_polynomial.X_mul_mod_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(i : σ)
(x : mv_polynomial σ R) :
(mv_polynomial.X i * x).mod_monomial (finsupp.single i 1) = 0
@[simp]
theorem
mv_polynomial.mul_X_mod_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R)
(i : σ) :
(x * mv_polynomial.X i).mod_monomial (finsupp.single i 1) = 0
@[simp]
theorem
mv_polynomial.mod_monomial_X
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(i : σ) :
(mv_polynomial.X i).mod_monomial (finsupp.single i 1) = 0
theorem
mv_polynomial.div_monomial_add_mod_monomial_single
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R)
(i : σ) :
mv_polynomial.X i * x.div_monomial (finsupp.single i 1) + x.mod_monomial (finsupp.single i 1) = x
theorem
mv_polynomial.mod_monomial_add_div_monomial_single
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
(x : mv_polynomial σ R)
(i : σ) :
x.mod_monomial (finsupp.single i 1) + mv_polynomial.X i * x.div_monomial (finsupp.single i 1) = x
theorem
mv_polynomial.X_dvd_iff_mod_monomial_eq_zero
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{i : σ}
{x : mv_polynomial σ R} :
mv_polynomial.X i ∣ x ↔ x.mod_monomial (finsupp.single i 1) = 0
Some results about dvd (∣) on monomial and X #
theorem
mv_polynomial.monomial_dvd_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{r s : R}
{i j : σ →₀ ℕ} :
@[simp]
theorem
mv_polynomial.monomial_one_dvd_monomial_one
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
[nontrivial R]
{i j : σ →₀ ℕ} :
⇑(mv_polynomial.monomial i) 1 ∣ ⇑(mv_polynomial.monomial j) 1 ↔ i ≤ j
@[simp]
theorem
mv_polynomial.X_dvd_X
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
[nontrivial R]
{i j : σ} :
mv_polynomial.X i ∣ mv_polynomial.X j ↔ i = j
@[simp]
theorem
mv_polynomial.X_dvd_monomial
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{i : σ}
{j : σ →₀ ℕ}
{r : R} :
mv_polynomial.X i ∣ ⇑(mv_polynomial.monomial j) r ↔ r = 0 ∨ ⇑j i ≠ 0