Theorems · Theorem · commutative algebra

MvPolynomial.support_sub_monomial_sub_monomial_subset

∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) [inst_1 : DecidableEq σ] (d d' : σ →₀ ℕ)
  (c : R),
  d ≠ d' →
    MvPolynomial.coeff d p = c →
      (p - ((MvPolynomial.monomial d) c - (MvPolynomial.monomial d') c)).support ⊆ p.support.erase d ∪ {d'}

Subtracting monomial d c - monomial d' c from p, where c = coeff d p and d ≠ d', leaves the support inside p.support.erase d ∪ {d'}.

Defined in

Mathlib.Algebra.MvPolynomial.CommRing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEq