Documentation

Mathlib.Algebra.MvPolynomial.Division

Division of MvPolynomial by monomials #

Main definitions #

Main results #

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

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

Equations
Instances For
    @[simp]
    theorem MvPolynomial.coeff_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ) (x : MvPolynomial σ R) (s' : σ →₀ ) :
    MvPolynomial.coeff s' (x.divMonomial s) = MvPolynomial.coeff (s + s') x
    @[simp]
    theorem MvPolynomial.support_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ) (x : MvPolynomial σ R) :
    (x.divMonomial s).support = x.support.preimage (fun (x : σ →₀ ) => s + x)
    @[simp]
    theorem MvPolynomial.zero_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ) :
    theorem MvPolynomial.divMonomial_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) :
    x.divMonomial 0 = x
    theorem MvPolynomial.add_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (y : MvPolynomial σ R) (s : σ →₀ ) :
    (x + y).divMonomial s = x.divMonomial s + y.divMonomial s
    theorem MvPolynomial.divMonomial_add {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ) (b : σ →₀ ) (x : MvPolynomial σ R) :
    x.divMonomial (a + b) = (x.divMonomial a).divMonomial b
    @[simp]
    theorem MvPolynomial.divMonomial_monomial_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ) (x : MvPolynomial σ R) :
    ((MvPolynomial.monomial a) 1 * x).divMonomial a = x
    @[simp]
    theorem MvPolynomial.divMonomial_mul_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ) (x : MvPolynomial σ R) :
    (x * (MvPolynomial.monomial a) 1).divMonomial a = x
    @[simp]
    theorem MvPolynomial.divMonomial_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (a : σ →₀ ) :
    ((MvPolynomial.monomial a) 1).divMonomial a = 1
    noncomputable def MvPolynomial.modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ) :

    The remainder upon division by monomial 1 s.

    Equations
    Instances For
      @[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' (x.modMonomial 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' (x.modMonomial s) = 0
      @[simp]
      theorem MvPolynomial.monomial_mul_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ) (x : MvPolynomial σ R) :
      ((MvPolynomial.monomial s) 1 * x).modMonomial s = 0
      @[simp]
      theorem MvPolynomial.mul_monomial_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ) (x : MvPolynomial σ R) :
      (x * (MvPolynomial.monomial s) 1).modMonomial s = 0
      @[simp]
      theorem MvPolynomial.monomial_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (s : σ →₀ ) :
      ((MvPolynomial.monomial s) 1).modMonomial s = 0
      theorem MvPolynomial.divMonomial_add_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ) :
      (MvPolynomial.monomial s) 1 * x.divMonomial s + x.modMonomial s = x
      theorem MvPolynomial.modMonomial_add_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (s : σ →₀ ) :
      x.modMonomial s + (MvPolynomial.monomial s) 1 * x.divMonomial 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 x.modMonomial i = 0
      @[simp]
      theorem MvPolynomial.X_mul_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) (x : MvPolynomial σ R) :
      (MvPolynomial.X i * x).divMonomial (Finsupp.single i 1) = x
      @[simp]
      theorem MvPolynomial.X_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) :
      (MvPolynomial.X i).divMonomial (Finsupp.single i 1) = 1
      @[simp]
      theorem MvPolynomial.mul_X_divMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (i : σ) :
      (x * MvPolynomial.X i).divMonomial (Finsupp.single i 1) = x
      @[simp]
      theorem MvPolynomial.X_mul_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) (x : MvPolynomial σ R) :
      (MvPolynomial.X i * x).modMonomial (Finsupp.single i 1) = 0
      @[simp]
      theorem MvPolynomial.mul_X_modMonomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (i : σ) :
      (x * MvPolynomial.X i).modMonomial (Finsupp.single i 1) = 0
      @[simp]
      theorem MvPolynomial.modMonomial_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) :
      (MvPolynomial.X i).modMonomial (Finsupp.single 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 * x.divMonomial (Finsupp.single i 1) + x.modMonomial (Finsupp.single i 1) = x
      theorem MvPolynomial.modMonomial_add_divMonomial_single {σ : Type u_1} {R : Type u_2} [CommSemiring R] (x : MvPolynomial σ R) (i : σ) :
      x.modMonomial (Finsupp.single i 1) + MvPolynomial.X i * x.divMonomial (Finsupp.single 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 x.modMonomial (Finsupp.single 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 : σ →₀ } :
      @[simp]
      theorem MvPolynomial.X_dvd_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nontrivial R] {i : σ} {j : σ} :
      @[simp]
      theorem MvPolynomial.X_dvd_monomial {σ : Type u_1} {R : Type u_2} [CommSemiring R] {i : σ} {j : σ →₀ } {r : R} :