Theorems · Theorem · field theory

Polynomial.div_prod_eq_quo_add_sum_rem_div

∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {ι : Type u_3} {g : ι → Polynomial R} {s : Finset ι},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

Let R be an integral domain and f : R[X]. Let s be a finite index set. Then a fraction of the form f / ∏ i ∈ s, g i evaluated in a field K containing R[X] can be rewritten as q + ∑ i ∈ s, r i / g i, where degree (r i) < degree (g i), provided that the g i are monic and pairwise coprime. See quo_add_sum_rem_div_unique for the uniqueness of this representation.

Defined in

Mathlib.Algebra.Polynomial.PartialFractions

Cited by

2 results in Mathlib

Foundations

Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldAlgebraFaithfulSMul