Theorems · Definition · commutative algebra

MvPolynomial.degrees

{R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → MvPolynomial σ R → Multiset σ

The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset. (For example, degrees (x^2 * y + y^3) would be {x, x, y, y, y}.)

Defined in

Mathlib.Algebra.MvPolynomial.Degrees

Cited by

51 results in Mathlib

Foundations

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

Assumes

CommSemiring