Theorems · Theorem · field theory

Polynomial.quo_mul_prod_add_sum_rem_mul_prod_unique

∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ {q₁ q₂ : Polynomial R} {r₁ r₂ : ι → Polynomial R},
        (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
          (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
            q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
                q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
              q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

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) in at most one way, where degree (r i) < degree (g i) and the denominator cancels formally. See eq_quo_mul_prod_add_sum_rem_mul_prod for the existence of such a representation.

Defined in

Mathlib.Algebra.Polynomial.PartialFractions

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEq