theorem MvPolynomial.degrees_eq_zero_iff_support_subset_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} : p.degrees = 0 ↔ p.support ⊆ {0}

@[simp]

theorem MvPolynomial.degreeOf_X_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] [Nontrivial R] (i : σ) : degreeOf i (X i) = 1

theorem MvPolynomial.ne_zero_of_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} : degreeOf i p ≠ 0 → p ≠ 0

@[simp]

theorem MvPolynomial.degreeOf_X_self_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] [Nontrivial R] (i : σ) (k : ℕ) : degreeOf i (X i ^ k) = k

theorem MvPolynomial.le_degreeOf_of_mem_support {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) {s : σ →₀ ℕ} : s ∈ p.support → s i ≤ degreeOf i p

theorem MvPolynomial.notMem_support_of_degreeOf_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) {s : σ →₀ ℕ} : degreeOf i p < s i → s ∉ p.support

theorem MvPolynomial.degreeOf_X_pow_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i j : σ} (k : ℕ) (h : i ≠ j) : degreeOf i (X j ^ k) = 0

theorem MvPolynomial.degreeOf_X_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {i j : σ} (h : i ≠ j) : degreeOf i (X j) = 0

theorem MvPolynomial.degreeOf_mul_X_self_pow_eq_add_of_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) (k : ℕ) (h : p ≠ 0) : degreeOf i (p * X i ^ k) = degreeOf i p + k

theorem MvPolynomial.degreeOf_mul_X_pow_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {i j : σ} (k : ℕ) (h : i ≠ j) : degreeOf i (p * X j ^ k) = degreeOf i p

theorem MvPolynomial.degreeOf_add_eq_of_degreeOf_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p q : MvPolynomial σ R} {i : σ} (h : degreeOf i q < degreeOf i p) : degreeOf i (p + q) = degreeOf i p

theorem MvPolynomial.degreeOf_eq_of_degreeOf_add_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p q : MvPolynomial σ R} {i : σ} (h : degreeOf i (p + q) < degreeOf i p) : degreeOf i p = degreeOf i q

theorem MvPolynomial.mem_vars_iff_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} : i ∈ p.vars ↔ degreeOf i p ≠ 0

theorem MvPolynomial.support_subset_vars_of_mem_support {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {s : σ →₀ ℕ} (h : s ∈ p.support) : s.support ⊆ p.vars

theorem MvPolynomial.vars_eq_empty_iff_eq_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} : p.vars = ∅ ↔ p = C (coeff 0 p)