English
In a polynomial ring over a domain, division with remainder holds against a monic divisor after mapping to a field of fractions.
Русский
В кольце полиномов над доменом существует деление с остатком на моническом делителе после отображения в поле дробей.
LaTeX
$$$\text{For } f \in R[x],\; g \text{ monic in } R[x],\; \exists q,r \in R[x]:\deg(r)<\deg(g)\text{ and } (f/g)=(q)+(r/g)\text{ in the fraction field.}$$$
Lean4
theorem div_eq_quo_add_rem_div (f : R[X]) {g : R[X]} (hg : g.Monic) :
∃ q r : R[X],
r.degree < g.degree ∧
(algebraMap R[X] K f) / (algebraMap R[X] K g) =
algebraMap R[X] K q + (algebraMap R[X] K r) / (algebraMap R[X] K g) :=
by
refine ⟨f /ₘ g, f %ₘ g, ?_, ?_⟩
· exact degree_modByMonic_lt _ hg
· have hg' : algebraMap R[X] K g ≠ 0 := (map_ne_zero_iff _ (IsFractionRing.injective R[X] K)).mpr (Monic.ne_zero hg)
field_simp
rw [add_comm, ← map_mul, ← map_add, modByMonic_add_div f hg]
