Theorems · Theorem · field theory

Polynomial.quo_add_sum_rem_mul_pow_inverse_unique

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : CommRing K] [inst_2 : Algebra (Polynomial R) K]
  [FaithfulSMul (Polynomial R) K] {ι : Type u_3} {s : Finset ι} {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ {n : ι → ℕ} {gi : ι → K},
        (∀ i ∈ s, gi i * (algebraMap (Polynomial R) K) (g i) = 1) →
          ∀ {q₁ q₂ : Polynomial R} {r₁ r₂ : (i : ι) → Fin (n i) → Polynomial R},
            (∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree) →
              (∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree) →
                (algebraMap (Polynomial R) K) q₁ +
                      ∑ i ∈ s, ∑ j, (algebraMap (Polynomial R) K) (r₁ i j) * gi i ^ (↑j + 1) =
                    (algebraMap (Polynomial R) K) q₂ +
                      ∑ i ∈ s, ∑ j, (algebraMap (Polynomial R) K) (r₂ i j) * gi i ^ (↑j + 1) →
                  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, and for each g i let n i be a natural number. Let K be an algebra over R[X] containing inverses gi i for each g i. Then a fraction of the form f * ∏ i ∈ s, gi i ^ n i can be rewritten as q + ∑ i ∈ s, ∑ j : Fin (n i), r i j * gi i ^ (j + 1) in at most one way, where degree (r i j) < degree (g i). See mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse for the existence of such a representation.

Defined in

Mathlib.Algebra.Polynomial.PartialFractions

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFaithfulSMul