def MonomialOrder.withBotDegree {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : WithBot (σ →₀ ℕ)

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

Equations

• m.withBotDegree f = WithBot.map (⇑m.toSyn.symm) (Finset.image (⇑m.toSyn) f.support).max

def MonomialOrder.toWithBotSyn {σ : Type u_1} (m : MonomialOrder σ) : WithBot (σ →₀ ℕ) ≃+ WithBot m.syn

Equations

• m.toWithBotSyn = m.toSyn.withBotCongr

@[simp]

theorem MonomialOrder.toWithBotSyn_apply_bot {σ : Type u_1} {m : MonomialOrder σ} : m.toWithBotSyn ⊥ = ⊥

@[simp]

theorem MonomialOrder.toWithBotSyn_symm_apply_bot {σ : Type u_1} {m : MonomialOrder σ} : m.toWithBotSyn.symm ⊥ = ⊥

@[simp]

theorem MonomialOrder.toWithBotSyn_apply_eq_bot_iff {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot (σ →₀ ℕ)) : m.toWithBotSyn a = ⊥ ↔ a = ⊥

@[simp]

theorem MonomialOrder.toWithBotSyn_symm_apply_eq_bot {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot m.syn) : m.toWithBotSyn.symm a = ⊥ ↔ a = ⊥

theorem MonomialOrder.toWithBotSyn_apply {σ : Type u_1} {m : MonomialOrder σ} (a : WithBot (σ →₀ ℕ)) : m.toWithBotSyn a = WithBot.map (⇑m.toSyn) a

def MonomialOrder.«term_≺'[_]_» : Lean.TrailingParserDescr

Given a monomial order with bot, notation for the corresponding strict order relation on WithBot (σ →₀ ℕ)

Equations

• One or more equations did not get rendered due to their size.

def MonomialOrder.«term_≼'[_]_» : Lean.TrailingParserDescr

Given a monomial order with bot, notation for the corresponding order relation on WithBot (σ →₀ ℕ)

Equations

• One or more equations did not get rendered due to their size.

theorem MonomialOrder.withBotDegree_eq {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) [Decidable (f = 0)] : m.withBotDegree f = if f = 0 then ⊥ else ↑(m.degree f)

@[simp]

theorem MonomialOrder.withBotDegree_eq_coe_degree_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : m.withBotDegree f = ↑(m.degree f) ↔ f ≠ 0

@[simp]

theorem MonomialOrder.withBotDegree_eq_bot_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : m.withBotDegree f = ⊥ ↔ f = 0

theorem MonomialOrder.degree_eq_unbotD_withBotDegree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

@[simp]

theorem MonomialOrder.withBotDegree_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] : m.withBotDegree 0 = ⊥

theorem MonomialOrder.withBotDegree_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (d : σ →₀ ℕ) (c : R) [Decidable (c = 0)] : m.withBotDegree ((MvPolynomial.monomial d) c) = if c = 0 then ⊥ else ↑d

theorem MonomialOrder.withBotDegree_C {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (c : R) [Decidable (c = 0)] : m.withBotDegree (MvPolynomial.C c) = if c = 0 then ⊥ else 0

@[simp]

theorem MonomialOrder.withBotDegree_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : m.withBotDegree (m.leadingTerm f) = m.withBotDegree f

@[simp]

theorem MonomialOrder.withBotDegree_neg {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommRing R] (f : MvPolynomial σ R) : m.withBotDegree (-f) = m.withBotDegree f

@[simp]

theorem MonomialOrder.withBotDegree_one {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Nontrivial R] : m.withBotDegree 1 = 0

theorem MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} (hf : m.leadingCoeff f ∈ nonZeroDivisors R) : f ∈ nonZeroDivisors (MvPolynomial σ R)

theorem MonomialOrder.withBotDegree_mul_of_left_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : m.leadingCoeff f ∈ nonZeroDivisors R) : m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

theorem MonomialOrder.withBotDegree_mul_of_right_mem_nonZeroDivisors {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} (hf : m.leadingCoeff g ∈ nonZeroDivisors R) : m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

@[simp]

theorem MonomialOrder.withBotDegree_mul {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) [NoZeroDivisors R] : m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

theorem MonomialOrder.withBotDegree_le_withBotDegree_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) : m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

theorem MonomialOrder.withBotDegree_le_withBotDegree_iff_of_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) {g : MvPolynomial σ R} (hg : g ≠ 0) : m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

theorem MonomialOrder.withBotDegree_lt_withBotDegree_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) : m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

theorem MonomialOrder.withBotDegree_eq_withBotDegree_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) : m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

theorem MonomialOrder.withBotDegree_add_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) : m.toWithBotSyn (m.withBotDegree (f + g)) ≤ max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

theorem and_iff_and_left_imp {a b : Prop} : a ∧ b ↔ a ∧ (a → b)

theorem MonomialOrder.withBotDegree_add_of_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) (h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)) : m.withBotDegree (f + g) = m.withBotDegree f

theorem MonomialOrder.withBotDegree_add_of_right_lt {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f g : MvPolynomial σ R) (h : m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g)) : m.withBotDegree (f + g) = m.withBotDegree g

theorem MonomialOrder.withBotDegree_sum_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {α : Type u_3} {s : Finset α} {f : α → MvPolynomial σ R} : m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun (x : α) => m.toWithBotSyn (m.withBotDegree (f x))

theorem MonomialOrder.le_withBotDegree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : d ∈ f.support) : m.toWithBotSyn ↑d ≤ m.toWithBotSyn (m.withBotDegree f)