@[deprecated MonomialOrder.leadingCoeff_mul (since := "2026-08-16")]
theorem
MonomialOrder.leadingCoeff_mul'
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_2}
[CommSemiring R]
[NoZeroDivisors R]
{f g : MvPolynomial σ R}
:
Alias of MonomialOrder.leadingCoeff_mul.
@[deprecated MonomialOrder.toSyn_degree_mul_le (since := "2026-08-16")]
theorem
MonomialOrder.degree_mul_le'
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_2}
[CommSemiring R]
{f g : MvPolynomial σ R}
:
Alias of MonomialOrder.toSyn_degree_mul_le.
theorem
MonomialOrder.sPolynomial_decomposition_of_degree_sum_smul_le₀
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_4}
[CommRing R]
{d : m.syn}
{ι : Type u_3}
{B : Finset ι}
{c : ι → R}
{g : ι → MvPolynomial σ R}
(hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
(hfd : m.toSyn (m.degree (∑ b ∈ B, c b • g b)) < d)
:
∃ (c' : ι → ι → R), ∑ b ∈ B, c b • g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c' b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
theorem
MonomialOrder.sPolynomial_decomposition_of_degree_sum_smul_le
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_4}
[CommRing R]
{d : m.syn}
{ι : Type u_3}
{B : Finset ι}
{c : ι → R}
{g : ι → MvPolynomial σ R}
(hB : ∀ b ∈ B, IsUnit (m.leadingCoeff (g b)))
(hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d)
(hfd : m.toSyn (m.degree (∑ b ∈ B, c b • g b)) < d)
:
∃ (c' : ι → ι → R), ∑ b ∈ B, c b • g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c' b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
theorem
MonomialOrder.sPolynomial_decomposition_of_degree_sum_le
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_4}
[CommRing R]
{d : m.syn}
{ι : Type u_3}
{B : Finset ι}
{g : ι → MvPolynomial σ R}
(hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∧ IsUnit (m.leadingCoeff (g b)) ∨ g b = 0)
(hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d)
:
∃ (c : ι → ι → R), ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
theorem
MonomialOrder.sPolynomial_monomial_mul_of_mem_nonZeroDivisors
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{p₁ p₂ : MvPolynomial σ R}
(hp₁ : m.leadingCoeff p₁ ∈ nonZeroDivisors R)
(hp₂ : m.leadingCoeff p₂ ∈ nonZeroDivisors R)
(d₁ d₂ : σ →₀ ℕ)
(c₁ c₂ : R)
:
m.sPolynomial ((MvPolynomial.monomial d₁) c₁ * p₁) ((MvPolynomial.monomial d₂) c₂ * p₂) = (MvPolynomial.monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) * m.sPolynomial p₁ p₂
theorem
MonomialOrder.sPolynomial_monomial_mul_of_mem_nonZeroDivisors'
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{p₁ p₂ : MvPolynomial σ R}
(hp₁ : m.leadingCoeff p₁ ∈ nonZeroDivisors R)
(hp₂ : m.leadingCoeff p₂ ∈ nonZeroDivisors R)
(d₁ d₂ : σ →₀ ℕ)
(c₁ c₂ : R)
:
m.sPolynomial ((MvPolynomial.monomial d₁) c₁ * p₁) ((MvPolynomial.monomial d₂) c₂ * p₂) = (MvPolynomial.monomial
(m.degree ((MvPolynomial.monomial d₁) c₁ * p₁) ⊔ m.degree ((MvPolynomial.monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
(c₁ * c₂) * m.sPolynomial p₁ p₂
theorem
MonomialOrder.leadingCoeff_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)
:
theorem
MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors'
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_2}
[CommSemiring R]
{f g : MvPolynomial σ R}
(hg : m.leadingCoeff g ∈ nonZeroDivisors R)
:
theorem
MonomialOrder.support_add_of_leadingTerm_add_leadingTerm_eq_zero
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_2}
[CommSemiring R]
{p q : MvPolynomial σ R}
(h : m.leadingTerm p + m.leadingTerm q = 0)
(a : σ →₀ ℕ)
:
theorem
MonomialOrder.support_sub_of_leadingTerm_eq_leadingTerm
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_3}
[CommRing R]
{p q : MvPolynomial σ R}
(h : m.leadingTerm p = m.leadingTerm q)
(a : σ →₀ ℕ)
:
theorem
MonomialOrder.degree_rename_killCompl_le_degree
{σ : Type u_1}
{m : MonomialOrder σ}
{σ' : Type u_2}
{R : Type u_3}
[CommSemiring R]
{f : σ' → σ}
(hf : Function.Injective f)
{p : MvPolynomial σ R}
:
@[deprecated MonomialOrder.toWithBotSyn_withBotDegree_mul_le (since := "2026-08-16")]
theorem
MonomialOrder.withBotDegree_mul_le'
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_2}
[CommSemiring R]
(f g : MvPolynomial σ R)
:
m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g)
theorem
MonomialOrder.withBotDegree_le_withBotDegree_iff'
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_2}
[CommSemiring R]
(f g : MvPolynomial σ R)
:
theorem
MonomialOrder.withBotDegree_rename_killCompl_le_withBotDegree
{σ : Type u_1}
{m : MonomialOrder σ}
{R : Type u_2}
[CommSemiring R]
{σ' : Type u_3}
{f : σ' → σ}
(hf : Function.Injective f)
(p : MvPolynomial σ R)
:
m.toWithBotSyn (m.withBotDegree ((MvPolynomial.rename f) ((MvPolynomial.killCompl hf) p))) ≤ m.toWithBotSyn (m.withBotDegree p)