Partial fractions

For f, g : R[X], if g is expressed as a product g₁ ^ n₁ * g₂ ^ n₂ * ... * gₙ ^ nₙ, where the gᵢ are monic and pairwise coprime, then there is a quotient q and for each i from 1 to n and for each 0 ≤ j < nᵢ there is a remainder rᵢⱼ with degree less than the degree of gᵢ, such that the fraction f / g decomposes as q + ∑ i j, rᵢⱼ / gᵢ ^ (j + 1).

Since polynomials do not have a division, the main theorem mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse is stated in an R[X]-algebra K containing inverses giᵢ for each polynomial gᵢ occuring in the denominator.

These results were formalised by the Xena Project, at the suggestion of Patrick Massot.

Main results

• mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse: Partial fraction decomposition for polynomials over a commutative ring R, the denomiator is a product of powers of monic pairwise coprime polynomials. Division is done in an R[X]-algebra K containing inverses gi i for each g i occuring in the denomiator.
• eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow: Partial fraction decomposition for polynomials over a commutative ring R, the denomiator is a product of powers of monic pairwise coprime polynomials. The denominators are multiplied out on both sides and formally cancelled.
• eq_quo_mul_prod_add_sum_rem_mul_prod: Partial fraction decomposition for polynomials over a commutative ring R, the denomiator is a product of monic pairwise coprime polynomials. The denominators are multiplied out on both sides and formally cancelled.
• div_prod_eq_quo_add_sum_rem_div: Partial fraction decomposition for polynomials over an integral domain R, the denominator is a product of monic pairwise coprime polynomials. Division is done in a field K containing R[X].
• div_eq_quo_add_rem_div_add_rem_div: Partial fraction decomposition for polynomials over an integral domain R, the denominator is a product of two monic coprime polynomials. Division is done in a field K containing R[X].

Naming

The lemmas in this file proving existence of partial fraction decomposition all have conclusions of the form ∃ q r, degree r < degree g ∧ f / g = q + ∑ r / g. The names of these lemmas depict only the final equality f / g = q + ∑ r / g. They are named structurally, except the bound variable q is called quo (for quotient) and the bound variable r is called rem (for remainder), since they are the quotient and remainder of the division f / g. For example, div_prod_eq_quo_add_sum_rem_div has the conclusion

∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧
  ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

The name of the lemma only shows the final equality, and in order we have / (div), ∏ (prod), = (eq), q (quo), + (add), ∑ (sum), r i (rem), / (div).

Scope for Expansion

• Proving uniqueness of the decomposition

theorem Polynomial.eq_quo_mul_pow_add_sum_rem_mul_pow {R : Type u_1} [CommRing R] [Nontrivial R] (f : Polynomial R) {g : Polynomial R} (hg : g.Monic) (n : ℕ) : ∃ (q : Polynomial R) (r : Fin n → Polynomial R), (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i : Fin n, r i * g ^ ↑i

Let R be a commutative ring and f g : R[X]. Let n be a natural number. Then f can be written in the form g i ^ n * (q + ∑ i : Fin n, r i / g i ^ (i + 1)), where degree (r i) < degree (g i) and the denominator cancels formally.

theorem Polynomial.eq_quo_mul_prod_add_sum_rem_mul_prod {R : Type u_1} [CommRing R] [Nontrivial R] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} (f : Polynomial R) {g : ι → Polynomial R} (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) : ∃ (q : Polynomial R) (r : ι → Polynomial R), (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g 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. Then f can be written in the form (∏ i ∈ s, g i) * (q + ∑ i ∈ s, r i / g i), where degree (r i) < degree (g i) and the denominator cancels formally.

theorem Polynomial.eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow {R : Type u_1} [CommRing R] [Nontrivial R] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} (f : Polynomial R) {g : ι → Polynomial R} (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) (n : ι → ℕ) : ∃ (q : Polynomial R) (r : (i : ι) → Fin (n i) → Polynomial 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 : Fin (n i), 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.

theorem Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse {R : Type u_1} [CommRing R] [Nontrivial R] {K : Type u_2} [CommRing K] [Algebra (Polynomial R) K] {ι : Type u_3} {s : Finset ι} (f : Polynomial R) {g : ι → Polynomial R} (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) (n : ι → ℕ) {gi : ι → K} (hgi : ∀ i ∈ s, gi i * (algebraMap (Polynomial R) K) (g i) = 1) : ∃ (q : Polynomial R) (r : (i : ι) → Fin (n i) → Polynomial 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 : Fin (n i), (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).

theorem Polynomial.div_prod_eq_quo_add_sum_rem_div {R : Type u_1} [CommRing R] [Nontrivial R] (K : Type u_2) [Field K] [Algebra (Polynomial R) K] [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {ι : Type u_3} {g : ι → Polynomial R} {s : Finset ι} (hg : ∀ i ∈ s, (g i).Monic) (hcop : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) : ∃ (q : Polynomial R) (r : ι → Polynomial R), (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g 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, where degree (r i) < degree (g i), provided that the g i are monic and pairwise coprime.

@[deprecated Polynomial.div_prod_eq_quo_add_sum_rem_div (since := "2026-02-08")]

theorem div_eq_quo_add_sum_rem_div {R : Type u_1} [CommRing R] [Nontrivial R] (K : Type u_2) [Field K] [Algebra (Polynomial R) K] [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {ι : Type u_3} {g : ι → Polynomial R} {s : Finset ι} (hg : ∀ i ∈ s, (g i).Monic) (hcop : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) : ∃ (q : Polynomial R) (r : ι → Polynomial R), (∀ i ∈ s, (r i).degree < (g i).degree) ∧ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑(r i) / ↑(g i)

Alias of Polynomial.div_prod_eq_quo_add_sum_rem_div.

---

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, where degree (r i) < degree (g i), provided that the g i are monic and pairwise coprime.

theorem Polynomial.div_eq_quo_add_rem_div_add_rem_div {R : Type u_1} [CommRing R] [Nontrivial R] (K : Type u_2) [Field K] [Algebra (Polynomial R) K] [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {g₁ g₂ : Polynomial R} (hg₁ : g₁.Monic) (hg₂ : g₂.Monic) (hcoprime : IsCoprime g₁ g₂) : ∃ (q : Polynomial R) (r₁ : Polynomial R) (r₂ : Polynomial R), r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Let R be an integral domain and f, g₁, g₂ : R[X]. Let g₁ and g₂ be monic and coprime. Then ∃ q, r₁, r₂ : R[X] such that f / (g₁ * g₂) = q + r₁ / g₁ + r₂ / g₂ and degree rᵢ < degree gᵢ, where the equality is taken in a field K containing R[X].

@[deprecated Polynomial.div_eq_quo_add_rem_div_add_rem_div (since := "2026-02-08")]

theorem div_eq_quo_add_rem_div_add_rem_div {R : Type u_1} [CommRing R] [Nontrivial R] (K : Type u_2) [Field K] [Algebra (Polynomial R) K] [FaithfulSMul (Polynomial R) K] (f : Polynomial R) {g₁ g₂ : Polynomial R} (hg₁ : g₁.Monic) (hg₂ : g₂.Monic) (hcoprime : IsCoprime g₁ g₂) : ∃ (q : Polynomial R) (r₁ : Polynomial R) (r₂ : Polynomial R), r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Alias of Polynomial.div_eq_quo_add_rem_div_add_rem_div.

---

Let R be an integral domain and f, g₁, g₂ : R[X]. Let g₁ and g₂ be monic and coprime. Then ∃ q, r₁, r₂ : R[X] such that f / (g₁ * g₂) = q + r₁ / g₁ + r₂ / g₂ and degree rᵢ < degree gᵢ, where the equality is taken in a field K containing R[X].