English
Division by a set B of polynomials with unit leading coefficients yields g and r such that f equals the sum over B of b g_b plus r with degree constraints and a remainder condition for all b in B.
Русский
Разделение по множеству B полиномов с единичными ведущими коэффициентами даёт g и r так, что f = сумма b g_b + r с ограничениями по степеням и остатком.
LaTeX
$$$\\exists g : B \\to_0 \\mathrm{MvPolynomial}_{\\sigma,R},\\; \\exists r : \\mathrm{MvPolynomial}_{\\sigma,R},\\ f = \\sum_{b \\in B} (b) \\cdot g(b) + r \\land \\dots$$$
Lean4
/-- Division by a *set* of multivariate polynomials
whose leading coefficients are invertible with respect to a monomial order -/
theorem div_set {B : Set (MvPolynomial σ R)} (hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R) :
∃ (g : B →₀ (MvPolynomial σ R)) (r : MvPolynomial σ R),
f = Finsupp.linearCombination _ (fun (b : B) ↦ (b : MvPolynomial σ R)) g + r ∧
(∀ (b : B), m.degree ((b : MvPolynomial σ R) * (g b)) ≼[m] m.degree f) ∧
(∀ c ∈ r.support, ∀ b ∈ B, ¬(m.degree b ≤ c)) :=
by
obtain ⟨g, r, H⟩ := m.div (b := fun (p : B) ↦ p) (fun b ↦ hB b b.prop) f
exact ⟨g, r, H.1, H.2.1, fun c hc b hb ↦ H.2.2 c hc ⟨b, hb⟩⟩
