Theorems · Theorem · field theory

Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : CommRing K] [inst_2 : Algebra (Polynomial R) K]
  [Nontrivial R] {ι : Type u_3} {s : Finset ι} (f : Polynomial R) {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 r,
            (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
              (algebraMap (Polynomial R) K) f * ∏ i ∈ s, gi i ^ n i =
                (algebraMap (Polynomial R) K) q + ∑ i ∈ s, ∑ j, (algebraMap (Polynomial R) K) (r i j) * gi i ^ (↑j + 1)

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), where degree (r i j) < degree (g i). See mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse for the uniqueness of this representation.

Defined in

Mathlib.Algebra.Polynomial.PartialFractions

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraNontrivial