English
Let R be an integral domain and f,g1,g2 ∈ R[X] with g1,g2 monic and coprime. Then there exist q,r1,r2 ∈ R[X] such that
Русский
Пусть R — интегральное доменное кольцо, f,g1,g2 ∈ R[X], причем g1,g2 моничны и взаимно просты. Тогда существуют q,r1,r2 ∈ R[X] такие, что
LaTeX
$$$\exists q,r_1,r_2 \in R[X],\; r_1.degree < g_1.degree \land r_2.degree < g_2\,degree \land \left(\frac{f}{g_1 g_2}\right) = \frac{q}{1} + \frac{r_1}{g_1} + \frac{r_2}{g_2} \quad \text{в поле частичных дробей.}$$$
Lean4
/-- Let R be an integral domain and f, g₁, g₂ ∈ R[X]. Let g₁ and g₂ be monic and coprime.
Then, ∃ q, r₁, r₂ ∈ R[X] such that f / g₁g₂ = q + r₁/g₁ + r₂/g₂ and deg(r₁) < deg(g₁) and
deg(r₂) < deg(g₂).
-/
theorem div_eq_quo_add_rem_div_add_rem_div (f : R[X]) {g₁ g₂ : R[X]} (hg₁ : g₁.Monic) (hg₂ : g₂.Monic)
(hcoprime : IsCoprime g₁ g₂) :
∃ q r₁ r₂ : R[X],
r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ (f : K) / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂ :=
by
rcases hcoprime with ⟨c, d, hcd⟩
refine
⟨f * d /ₘ g₁ + f * c /ₘ g₂, f * d %ₘ g₁, f * c %ₘ g₂, degree_modByMonic_lt _ hg₁, degree_modByMonic_lt _ hg₂, ?_⟩
have hg₁' : (↑g₁ : K) ≠ 0 := by
norm_cast
exact hg₁.ne_zero
have hg₂' : (↑g₂ : K) ≠ 0 := by
norm_cast
exact hg₂.ne_zero
have hfc := modByMonic_add_div (f * c) hg₂
have hfd := modByMonic_add_div (f * d) hg₁
field_simp
norm_cast
linear_combination -1 * f * hcd + -1 * g₁ * hfc + -1 * g₂ * hfd
