Theorems · Theorem · commutative algebra

MonomialOrder.div

∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {ι : Type u_3} {b : ι → MvPolynomial σ R},
  (∀ (i : ι), IsUnit (m.leadingCoeff (b i))) →
    ∀ (f : MvPolynomial σ R),
      ∃ g r,
        f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
          (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
            ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Division by a family of multivariate polynomials whose leading coefficients are invertible with respect to a monomial order

Defined in

Mathlib.RingTheory.MvPolynomial.Groebner

Cited by

2 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing