English
Dividing by a single polynomial b with unit leading coefficient produces g and r such that f = g b + r, with deg(b g) ≤ deg(f) and a remainder property for r.
Русский
Деление на один полином b с единичным ведущим коэффициентом даёт g и r такие, что f = g b + r, deg(b g) ≤ deg f и остаток удовлетворяет условиям.
LaTeX
$$$\\exists g,r\\; (f = g b + r) \\land (m.deg(b g) \\preceq_m m.deg f) \\land (\\forall c \\in r.\\mathrm{support}, \\neg (m.deg b \\le c))$$$
Lean4
/-- Division by a multivariate polynomial
whose leading coefficient is invertible with respect to a monomial order -/
theorem div_single {b : MvPolynomial σ R} (hb : IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R) :
∃ (g : MvPolynomial σ R) (r : MvPolynomial σ R),
f = g * b + r ∧ (m.degree (b * g) ≼[m] m.degree f) ∧ (∀ c ∈ r.support, ¬(m.degree b ≤ c)) :=
by
obtain ⟨g, r, hgr, h1, h2⟩ := div_set (B := { b }) (m := m) (by simp [hb]) f
specialize h1 ⟨b, by simp⟩
set q := g ⟨b, by simp⟩
simp only [Set.mem_singleton_iff, forall_eq] at h2
simp only at h1
refine ⟨q, r, ?_, h1, h2⟩
rw [hgr]
simp only [Finsupp.linearCombination, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, smul_eq_mul,
add_left_inj]
rw [Finsupp.sum_eq_single ⟨b, by simp⟩ _ (by simp)]
simp +contextual
