Documentation

Mathlib.RingTheory.MvPolynomial.MonomialOrder

Degree and leading coefficient of polynomials with respect to a monomial order #

We consider a type σ of indeterminates and a commutative semiring R and a monomial order m : MonomialOrder σ.

Reference #

[BW93]

def MonomialOrder.degree {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) :

the degree of a multivariate polynomial with respect to a monomial ordering

Equations
Instances For
    def MonomialOrder.leadingCoeff {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) :
    R

    the leading coefficient of a multivariate polynomial with respect to a monomial ordering

    Equations
    Instances For
      @[deprecated MonomialOrder.leadingCoeff (since := "2025-01-31")]
      def MonomialOrder.lCoeff {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) :
      R

      Alias of MonomialOrder.leadingCoeff.


      the leading coefficient of a multivariate polynomial with respect to a monomial ordering

      Equations
      Instances For
        @[simp]
        theorem MonomialOrder.degree_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :
        m.degree 0 = 0
        @[simp]
        theorem MonomialOrder.leadingCoeff_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :
        @[deprecated MonomialOrder.leadingCoeff_zero (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] :

        Alias of MonomialOrder.leadingCoeff_zero.

        theorem MonomialOrder.degree_monomial_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ } (c : R) :
        theorem MonomialOrder.degree_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ } (c : R) [Decidable (c = 0)] :
        theorem MonomialOrder.degree_X_le_single {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {s : σ} :
        theorem MonomialOrder.degree_X {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Nontrivial R] {s : σ} :
        @[simp]
        theorem MonomialOrder.leadingCoeff_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ } (c : R) :
        @[deprecated MonomialOrder.leadingCoeff_monomial (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {d : σ →₀ } (c : R) :

        Alias of MonomialOrder.leadingCoeff_monomial.

        theorem MonomialOrder.degree_le_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ } :
        m.toSyn (m.degree f) m.toSyn d cf.support, m.toSyn c m.toSyn d
        theorem MonomialOrder.degree_lt_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ } (hd : m.toSyn 0 < m.toSyn d) :
        m.toSyn (m.degree f) < m.toSyn d cf.support, m.toSyn c < m.toSyn d
        theorem MonomialOrder.le_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ } (hd : d f.support) :
        m.toSyn d m.toSyn (m.degree f)
        theorem MonomialOrder.coeff_eq_zero_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ } (hd : m.toSyn (m.degree f) < m.toSyn d) :
        @[deprecated MonomialOrder.leadingCoeff_ne_zero_iff (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_ne_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} :

        Alias of MonomialOrder.leadingCoeff_ne_zero_iff.

        @[simp]
        theorem MonomialOrder.leadingCoeff_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} :
        m.leadingCoeff f = 0 f = 0
        @[deprecated MonomialOrder.leadingCoeff_eq_zero_iff (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} :
        m.leadingCoeff f = 0 f = 0

        Alias of MonomialOrder.leadingCoeff_eq_zero_iff.

        @[simp]
        theorem MonomialOrder.coeff_degree_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} :
        @[simp]
        theorem MonomialOrder.degree_C {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (r : R) :
        theorem MonomialOrder.eq_C_of_degree_eq_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (hf : m.degree f = 0) :
        theorem MonomialOrder.degree_add_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} :
        m.toSyn (m.degree (f + g)) m.toSyn (m.degree f) m.toSyn (m.degree g)
        theorem MonomialOrder.degree_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) :
        m.degree (f + g) = m.degree f
        theorem MonomialOrder.leadingCoeff_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) :
        @[deprecated MonomialOrder.leadingCoeff_add_of_lt (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) :

        Alias of MonomialOrder.leadingCoeff_add_of_lt.

        theorem MonomialOrder.degree_add_of_ne {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (h : m.degree f m.degree g) :
        m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f) m.toSyn (m.degree g)
        theorem MonomialOrder.degree_mul_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} :
        m.toSyn (m.degree (f * g)) m.toSyn (m.degree f + m.degree g)
        theorem MonomialOrder.coeff_mul_of_add_of_degree_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} {a b : σ →₀ } (ha : m.toSyn (m.degree f) m.toSyn a) (hb : m.toSyn (m.degree g) m.toSyn b) :

        Multiplicativity of leading coefficients

        theorem MonomialOrder.coeff_mul_of_degree_add {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} :

        Multiplicativity of leading coefficients

        theorem MonomialOrder.degree_mul_of_isRegular_left {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g 0) :
        m.degree (f * g) = m.degree f + m.degree g

        Multiplicativity of leading coefficients

        theorem MonomialOrder.leadingCoeff_mul_of_isRegular_left {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g 0) :

        Multiplicativity of leading coefficients

        @[deprecated MonomialOrder.leadingCoeff_mul_of_isRegular_left (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_mul_of_isRegular_left {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g 0) :

        Alias of MonomialOrder.leadingCoeff_mul_of_isRegular_left.


        Multiplicativity of leading coefficients

        theorem MonomialOrder.degree_mul_of_isRegular_right {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : f 0) (hg : IsRegular (m.leadingCoeff g)) :
        m.degree (f * g) = m.degree f + m.degree g

        Multiplicativity of leading coefficients

        theorem MonomialOrder.leadingCoeff_mul_of_isRegular_right {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : f 0) (hg : IsRegular (m.leadingCoeff g)) :

        Multiplicativity of leading coefficients

        @[deprecated MonomialOrder.leadingCoeff_mul_of_isRegular_right (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_mul_of_isRegular_right {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : f 0) (hg : IsRegular (m.leadingCoeff g)) :

        Alias of MonomialOrder.leadingCoeff_mul_of_isRegular_right.


        Multiplicativity of leading coefficients

        theorem MonomialOrder.degree_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : f 0) (hg : g 0) :
        m.degree (f * g) = m.degree f + m.degree g

        Degree of product

        theorem MonomialOrder.degree_mul_of_nonzero_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hfg : f * g 0) :
        m.degree (f * g) = m.degree f + m.degree g

        Degree of of product

        theorem MonomialOrder.leadingCoeff_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : f 0) (hg : g 0) :

        Multiplicativity of leading coefficients

        @[deprecated MonomialOrder.leadingCoeff_mul (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {f g : MvPolynomial σ R} (hf : f 0) (hg : g 0) :

        Alias of MonomialOrder.leadingCoeff_mul.


        Multiplicativity of leading coefficients

        theorem MonomialOrder.degree_smul_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : R} {f : MvPolynomial σ R} :
        m.toSyn (m.degree (r f)) m.toSyn (m.degree f)
        theorem MonomialOrder.degree_smul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : R} (hr : IsRegular r) {f : MvPolynomial σ R} :
        m.degree (r f) = m.degree f
        theorem MonomialOrder.degree_prod_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {P : ιMvPolynomial σ R} {s : Finset ι} :
        m.toSyn (m.degree (∏ is, P i)) m.toSyn (∑ is, m.degree (P i))
        theorem MonomialOrder.coeff_prod_sum_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} (P : ιMvPolynomial σ R) (s : Finset ι) :
        MvPolynomial.coeff (∑ is, m.degree (P i)) (∏ is, P i) = is, m.leadingCoeff (P i)
        theorem MonomialOrder.degree_prod_of_regular {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {P : ιMvPolynomial σ R} {s : Finset ι} (H : is, IsRegular (m.leadingCoeff (P i))) :
        m.degree (∏ is, P i) = is, m.degree (P i)
        theorem MonomialOrder.degree_prod {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [IsDomain R] {ι : Type u_3} {P : ιMvPolynomial σ R} {s : Finset ι} (H : is, P i 0) :
        m.degree (∏ is, P i) = is, m.degree (P i)
        theorem MonomialOrder.leadingCoeff_prod_of_regular {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} {P : ιMvPolynomial σ R} {s : Finset ι} (H : is, IsRegular (m.leadingCoeff (P i))) :
        m.leadingCoeff (∏ is, P i) = is, m.leadingCoeff (P i)
        @[simp]
        theorem MonomialOrder.degree_neg {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f : MvPolynomial σ R} :
        m.degree (-f) = m.degree f
        theorem MonomialOrder.degree_sub_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} :
        m.toSyn (m.degree (f - g)) m.toSyn (m.degree f) m.toSyn (m.degree g)
        theorem MonomialOrder.degree_sub_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) :
        m.degree (f - g) = m.degree f
        theorem MonomialOrder.leadingCoeff_sub_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) :
        @[deprecated MonomialOrder.leadingCoeff_sub_of_lt (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_sub_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {f g : MvPolynomial σ R} (h : m.toSyn (m.degree g) < m.toSyn (m.degree f)) :

        Alias of MonomialOrder.leadingCoeff_sub_of_lt.

        theorem MonomialOrder.isUnit_leadingCoeff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [Field R] {f : MvPolynomial σ R} :
        @[deprecated MonomialOrder.isUnit_leadingCoeff (since := "2025-01-31")]
        theorem MonomialOrder.lCoeff_is_unit_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [Field R] {f : MvPolynomial σ R} :

        Alias of MonomialOrder.isUnit_leadingCoeff.