mathlib3 documentation

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 #

Main results #

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 : σ →₀ ) :

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} [comm_semiring R] (s : σ →₀ ) (x : mv_polynomial σ R) (s' : σ →₀ ) :
@[simp]
theorem mv_polynomial.support_div_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (s : σ →₀ ) (x : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.zero_div_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (s : σ →₀ ) :
theorem mv_polynomial.div_monomial_zero {σ : Type u_1} {R : Type u_2} [comm_semiring R] (x : mv_polynomial σ R) :
theorem mv_polynomial.add_div_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (x y : mv_polynomial σ R) (s : σ →₀ ) :
theorem mv_polynomial.div_monomial_add {σ : Type u_1} {R : Type u_2} [comm_semiring R] (a b : σ →₀ ) (x : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.div_monomial_monomial_mul {σ : Type u_1} {R : Type u_2} [comm_semiring R] (a : σ →₀ ) (x : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.div_monomial_mul_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (a : σ →₀ ) (x : mv_polynomial σ R) :
@[simp]
noncomputable def mv_polynomial.mod_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (x : mv_polynomial σ 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} [comm_semiring R] {s' s : σ →₀ } (x : mv_polynomial σ R) (h : ¬s s') :
@[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') :
@[simp]
theorem mv_polynomial.monomial_mul_mod_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (s : σ →₀ ) (x : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.mul_monomial_mod_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (s : σ →₀ ) (x : mv_polynomial σ R) :
@[simp]
@[simp]
theorem mv_polynomial.X_mul_div_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (i : σ) (x : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.X_div_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (i : σ) :
@[simp]
theorem mv_polynomial.mul_X_div_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (x : mv_polynomial σ R) (i : σ) :
@[simp]
theorem mv_polynomial.X_mul_mod_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (i : σ) (x : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.mul_X_mod_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] (x : mv_polynomial σ R) (i : σ) :
@[simp]
theorem mv_polynomial.mod_monomial_X {σ : Type u_1} {R : Type u_2} [comm_semiring R] (i : σ) :

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.X_dvd_X {σ : Type u_1} {R : Type u_2} [comm_semiring R] [nontrivial R] {i j : σ} :
@[simp]
theorem mv_polynomial.X_dvd_monomial {σ : Type u_1} {R : Type u_2} [comm_semiring R] {i : σ} {j : σ →₀ } {r : R} :