# mathlib3documentation

data.mv_polynomial.division

# 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: divides x by the monomial mv_polynomial.monomial 1 s
• mv_polynomial.mod_monomial x s: the remainder upon dividing x by the monomial mv_polynomial.monomial 1 s.

## Main results #

• mv_polynomial.div_monomial_add_mod_monomial, mv_polynomial.mod_monomial_add_div_monomial: div_monomial and mod_monomial 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 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} (p : R) (s : σ →₀ ) :

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

Equations
@[simp]
theorem mv_polynomial.coeff_div_monomial {σ : Type u_1} {R : Type u_2} (s : σ →₀ ) (x : R) (s' : σ →₀ ) :
@[simp]
theorem mv_polynomial.support_div_monomial {σ : Type u_1} {R : Type u_2} (s : σ →₀ ) (x : R) :
@[simp]
theorem mv_polynomial.zero_div_monomial {σ : Type u_1} {R : Type u_2} (s : σ →₀ ) :
theorem mv_polynomial.div_monomial_zero {σ : Type u_1} {R : Type u_2} (x : R) :
theorem mv_polynomial.add_div_monomial {σ : Type u_1} {R : Type u_2} (x y : R) (s : σ →₀ ) :
theorem mv_polynomial.div_monomial_add {σ : Type u_1} {R : Type u_2} (a b : σ →₀ ) (x : R) :
@[simp]
theorem mv_polynomial.div_monomial_monomial_mul {σ : Type u_1} {R : Type u_2} (a : σ →₀ ) (x : R) :
1 * x).div_monomial a = x
@[simp]
theorem mv_polynomial.div_monomial_mul_monomial {σ : Type u_1} {R : Type u_2} (a : σ →₀ ) (x : R) :
(x * 1).div_monomial a = x
@[simp]
theorem mv_polynomial.div_monomial_monomial {σ : Type u_1} {R : Type u_2} (a : σ →₀ ) :
1).div_monomial a = 1
noncomputable def mv_polynomial.mod_monomial {σ : Type u_1} {R : Type u_2} (x : R) (s : σ →₀ ) :

The remainder upon division by monomial 1 s.

Equations
@[simp]
theorem mv_polynomial.coeff_mod_monomial_of_not_le {σ : Type u_1} {R : Type u_2} {s' s : σ →₀ } (x : R) (h : ¬s s') :
(x.mod_monomial s) =
@[simp]
theorem mv_polynomial.coeff_mod_monomial_of_le {σ : Type u_1} {R : Type u_2} {s' s : σ →₀ } (x : R) (h : s s') :
(x.mod_monomial s) = 0
@[simp]
theorem mv_polynomial.monomial_mul_mod_monomial {σ : Type u_1} {R : Type u_2} (s : σ →₀ ) (x : R) :
1 * x).mod_monomial s = 0
@[simp]
theorem mv_polynomial.mul_monomial_mod_monomial {σ : Type u_1} {R : Type u_2} (s : σ →₀ ) (x : R) :
(x * 1).mod_monomial s = 0
@[simp]
theorem mv_polynomial.monomial_mod_monomial {σ : Type u_1} {R : Type u_2} (s : σ →₀ ) :
1).mod_monomial s = 0
theorem mv_polynomial.div_monomial_add_mod_monomial {σ : Type u_1} {R : Type u_2} (x : R) (s : σ →₀ ) :
theorem mv_polynomial.mod_monomial_add_div_monomial {σ : Type u_1} {R : Type u_2} (x : R) (s : σ →₀ ) :
theorem mv_polynomial.monomial_one_dvd_iff_mod_monomial_eq_zero {σ : Type u_1} {R : Type u_2} {i : σ →₀ } {x : R} :
@[simp]
theorem mv_polynomial.X_mul_div_monomial {σ : Type u_1} {R : Type u_2} (i : σ) (x : R) :
* x).div_monomial 1) = x
@[simp]
theorem mv_polynomial.X_div_monomial {σ : Type u_1} {R : Type u_2} (i : σ) :
1) = 1
@[simp]
theorem mv_polynomial.mul_X_div_monomial {σ : Type u_1} {R : Type u_2} (x : R) (i : σ) :
(x * .div_monomial 1) = x
@[simp]
theorem mv_polynomial.X_mul_mod_monomial {σ : Type u_1} {R : Type u_2} (i : σ) (x : R) :
* x).mod_monomial 1) = 0
@[simp]
theorem mv_polynomial.mul_X_mod_monomial {σ : Type u_1} {R : Type u_2} (x : R) (i : σ) :
(x * .mod_monomial 1) = 0
@[simp]
theorem mv_polynomial.mod_monomial_X {σ : Type u_1} {R : Type u_2} (i : σ) :
1) = 0
theorem mv_polynomial.div_monomial_add_mod_monomial_single {σ : Type u_1} {R : Type u_2} (x : R) (i : σ) :
theorem mv_polynomial.mod_monomial_add_div_monomial_single {σ : Type u_1} {R : Type u_2} (x : R) (i : σ) :
theorem mv_polynomial.X_dvd_iff_mod_monomial_eq_zero {σ : Type u_1} {R : Type u_2} {i : σ} {x : R} :

### Some results about dvd (∣) on monomial and X#

theorem mv_polynomial.monomial_dvd_monomial {σ : Type u_1} {R : Type u_2} {r s : R} {i j : σ →₀ } :
(s = 0 i j) r s
@[simp]
theorem mv_polynomial.monomial_one_dvd_monomial_one {σ : Type u_1} {R : Type u_2} [nontrivial R] {i j : σ →₀ } :
i j
@[simp]
theorem mv_polynomial.X_dvd_X {σ : Type u_1} {R : Type u_2} [nontrivial R] {i j : σ} :
i = j
@[simp]
theorem mv_polynomial.X_dvd_monomial {σ : Type u_1} {R : Type u_2} {i : σ} {j : σ →₀ } {r : R} :
r = 0 j i 0