Theorems · Theorem · field theory

Polynomial.quo_add_sum_rem_div_unique

∀ {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] {ι : Type u_3} {g : ι → Polynomial R} {s : Finset ι},
  (∀ 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, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i) → q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ 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 in at most one way, where degree (r i) < degree (g i), provided that the g i are monic and pairwise coprime. See div_prod_eq_quo_add_sum_rem_div for the existence of such a representation.

Defined in

Mathlib.Algebra.Polynomial.PartialFractions

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraFaithfulSMul