Documentation

CharacteristicSet.MainDegree

Main degree of a polynomial #

MvPolynomial.mainDegree p is the multiset of occurrences of the maximal variable of p. Its cardinality is the degree in that variable; it is empty for constants and zero.

The definition and lemmas are ported from the Degrees and Variables modules in SnkXyx/mathlib4 at b7f37486b1c723b65299b4fd7ad635131674d9e8.

source
@[instance_reducible]
noncomputable instance MvPolynomial.decidablePredIsMaxOnDegrees {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} :
DecidablePred (IsMaxOn id ↑p.degrees.toFinset)
Equations
source
noncomputable def MvPolynomial.mainDegree {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) :
Multiset σ

When σ is a linear order, mainDegree p is the multiset consisting of the maximal variable among all variables appearing in p, appearing with its largest multiplicity among all monomials in p.

For example, mainDegree (x^2 * y + x * y^3) is {y, y, y} when x < y.

Equations
Instances For
    source
    theorem MvPolynomial.mainDegree_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) :
    p.mainDegree = Multiset.filter (IsMaxOn id ↑p.degrees.toFinset) p.degrees
    source
    theorem MvPolynomial.forall_mainDegree_eq_of_forall_degrees_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {i : σ} {p : MvPolynomial σ R} (h1 : i ∈ p.degrees) (h2 : IsMaxOn id (↑p.degrees.toFinset) i) (j : σ) :
    j ∈ p.mainDegree → i = j
    source
    theorem MvPolynomial.card_mainDegree_eq_degreeOf_of_forall_degrees_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {i : σ} {p : MvPolynomial σ R} (h1 : i ∈ p.degrees) (h2 : IsMaxOn id (↑p.degrees.toFinset) i) :
    p.mainDegree.card = degreeOf i p
    source
    @[simp]
    theorem MvPolynomial.mainDegree_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] :
    mainDegree 0 = 0
    source
    theorem MvPolynomial.mainDegree_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (r : R) :
    (C r).mainDegree = 0
    source
    @[simp]
    theorem MvPolynomial.mainDegree_X {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] (i : σ) :
    (X i).mainDegree = {i}
    source
    theorem MvPolynomial.card_mainDegree_eq_degreeOf {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {c : σ} {p : MvPolynomial σ R} (h : p.vars.max = ↑c) :
    p.mainDegree.card = degreeOf c p
    source
    theorem MvPolynomial.card_mainDegree_eq_zero_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} :
    p.mainDegree.card = 0 ↔ p.vars.max = ⊥