Theorems · Theorem · commutative algebra

MvPolynomial.degreeOf_eq_natDegree

∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (a : σ) (p : MvPolynomial σ R),
  MvPolynomial.degreeOf a p =
    ((MvPolynomial.optionEquivLeft R { b // b ≠ a })
        ((MvPolynomial.rename ⇑(Equiv.optionSubtypeNe a).symm) p)).natDegree

The MvPolynomial.degreeOf of a particular variable in a multivariate polynomial is equal to the Polynomial.natDegree of the single-variable polynomial obtained by treating the multivariable polynomial as a single variable polynomial over multivariable polynomials in the remaining variables

Defined in

Mathlib.Algebra.MvPolynomial.Equiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidableEq