Theorems · Theorem · field theory

Polynomial.eq_quo_mul_prod_add_sum_rem_mul_prod

∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R] {ι : Type u_2} [inst_2 : DecidableEq ι] {s : Finset ι}
  (f : Polynomial R) {g : ι → Polynomial R},
  (∀ 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 = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k

Let R be a commutative ring and f : R[X]. Let s be a finite index set. Let g i be a collection of monic and pairwise coprime polynomials indexed by s. Then f can be written in the form (∏ i ∈ s, g i) * (q + ∑ i ∈ s, r i / g i), where degree (r i) < degree (g i) and the denominator cancels formally. See quo_mul_prod_add_sum_rem_mul_prod_unique for the uniqueness of this representation.

Defined in

Mathlib.Algebra.Polynomial.PartialFractions

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingNontrivialDecidableEq