Theorems · Theorem · field theory

Polynomial.eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow

∀ {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)) →
      ∀ (n : ι → ℕ),
        ∃ q r,
          (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
            f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n 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, and for each g i let n i be a natural number. Then f can be written in the form (∏ i ∈ s, g i ^ n i) * (q + ∑ i ∈ s, ∑ j : Fin (n i), r i j / g i ^ (j + 1)), where degree (r i j) < degree (g i) and the denominator cancels formally. See quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique for the uniqueness of this representation.

Defined in

Mathlib.Algebra.Polynomial.PartialFractions

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingNontrivialDecidableEq