div_eq_quo_add_sum_rem_div — Mathlib

English

Let R be an integral domain and f ∈ R[X]. Let s be a finite index set, and let g_i ∈ R[X] (i ∈ s) be monic with the g_i pairwise coprime. Then there exist q ∈ R[X] and r_i ∈ R[X] (i ∈ s) such that deg(r_i) < deg(g_i) for all i ∈ s, and in the fraction field K of R[X] one has f / ∏_{i∈s} g_i = q + ∑_{i∈s} (r_i / g_i).

Русский

Пусть R — интегральная область, f ∈ R[x]. Пусть s — конечный индексный множество и для каждого i ∈ s полином g_i ∈ R[x] моноический, причём g_i попарно неприводимы на взаимно простые. Тогда существуют q ∈ R[x] и r_i ∈ R[x] (i ∈ s) такие, что deg(r_i) < deg(g_i) для всех i, и в полей дробей K над R[x] выполняется f / ∏_{i∈s} g_i = q + ∑_{i∈s} r_i / g_i.

LaTeX

$$$\\exists q \\in R[X], \\exists r : ι \\to R[X],\\; (\\forall i \\in s, \\deg(r_i) < \\deg(g_i)) \\land \\left(\\left(\\uparrow f : K\\right) / \\prod_{i \\in s} \\uparrow(g_i)\\right) = \\uparrow q + \\sum_{i \\in s} (r_i : K) / (g_i : K) \\quad \\text{in } K.$$$

Lean4

/-- Let R be an integral domain and f ∈ R[X]. Let s be a finite index set.
Then, a fraction of the form f / ∏ (g i) can be rewritten as q + ∑ (r i) / (g i), where
deg(r i) < deg(g i), provided that the g i are monic and pairwise coprime.
-/
theorem div_eq_quo_add_sum_rem_div (f : R[X]) {ι : Type*} {g : ι → R[X]} {s : Finset ι} (hg : ∀ i ∈ s, (g i).Monic)
    (hcop : Set.Pairwise ↑s fun i j => IsCoprime (g i) (g j)) :
    ∃ (q : R[X]) (r : ι → R[X]),
      (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ((↑f : K) / ∏ i ∈ s, ↑(g i)) = ↑q + ∑ i ∈ s, (r i : K) / (g i : K) :=
  by
  classical
  induction s using Finset.induction_on generalizing f with
  | empty =>
    refine ⟨f, fun _ : ι => (0 : R[X]), fun i => ?_, by simp⟩
    rintro ⟨⟩
  | insert a b hab Hind => ?_
  obtain ⟨q₀, r₁, r₂, hdeg₁, _, hf : (↑f : K) / _ = _⟩ :=
    div_eq_quo_add_rem_div_add_rem_div R K f (hg a (b.mem_insert_self a) : Monic (g a))
      (monic_prod_of_monic _ _ fun i hi => hg i (Finset.mem_insert_of_mem hi) : Monic (∏ i ∈ b, g i))
      (IsCoprime.prod_right fun i hi =>
        hcop (Finset.mem_coe.2 (b.mem_insert_self a)) (Finset.mem_coe.2 (Finset.mem_insert_of_mem hi))
          (by rintro rfl; exact hab hi))
  obtain ⟨q, r, hrdeg, IH⟩ :=
    Hind _ (fun i hi => hg i (Finset.mem_insert_of_mem hi))
      (Set.Pairwise.mono (Finset.coe_subset.2 fun i hi => Finset.mem_insert_of_mem hi) hcop)
  refine ⟨q₀ + q, fun i => if i = a then r₁ else r i, ?_, ?_⟩
  · intro i
    dsimp only
    split_ifs with h1
    · cases h1
      intro
      exact hdeg₁
    · intro hi
      exact hrdeg i (Finset.mem_of_mem_insert_of_ne hi h1)
  norm_cast at hf IH ⊢
  rw [Finset.prod_insert hab, hf, IH, Finset.sum_insert hab, if_pos rfl]
  trans (↑(q₀ + q : R[X]) : K) + (↑r₁ / ↑(g a) + ∑ i ∈ b, (r i : K) / (g i : K))
  · push_cast
    ring
  congr 2
  refine Finset.sum_congr rfl fun x hxb => ?_
  grind

Похожие утверждения