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).

The lemmas in this file proving uniqueness of partial fraction decomposition all have conclusions of the form q₁ + ∑ r₁ / g = q₂ + ∑ r₂ / g → q₁ = q₂ ∧ r₁ = r₂. The names of these lemmas show a side of the equality hypothesis q₁ + ∑ r₁ / g = q₂ + ∑ r₂ / g, and are suffixed by _unique. In analogy with the existence lemmas, the variables qᵢ are called quotients and referred to as quo in the name of the lemma and the variables rᵢ are called remainders and referred to as rem in the name of the lemma. For example, quo_add_sum_rem_div_unique has the conclusion

↑q₁ + ∑ i ∈ s, ↑(r₁ i) / ↑(g i) = ↑q₂ + ∑ i ∈ s, ↑(r₂ i) / ↑(g i)) →
  q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i

The name of the lemmas shows one side of the equality hypothesis (the other is the same), and in order we have q (quo), + (add), ∑ (sum), r i (rem), / (div).

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 ^ n * (q + ∑ i : Fin n, r i / g ^ (i + 1)), where degree (r i) < degree g and the denominator cancels formally. See quo_mul_pow_add_sum_rem_mul_pow_unique for the uniqueness of this representation.

theorem Polynomial.quo_mul_pow_add_sum_rem_mul_pow_unique {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) {n : ℕ} {q₁ q₂ : Polynomial R} {r₁ r₂ : Fin n → Polynomial R} (hr₁ : ∀ (i : Fin n), (r₁ i).degree < g.degree) (hr₂ : ∀ (i : Fin n), (r₂ i).degree < g.degree) (hf : q₁ * g ^ n + ∑ i : Fin n, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i : Fin n, r₂ i * g ^ ↑i) : q₁ = q₂ ∧ r₁ = r₂

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 ^ n * (q + ∑ i : Fin n, r i / g ^ (i + 1)) in at most one way, where degree (r i) < degree g and the denominator cancels formally. See eq_quo_mul_pow_add_sum_rem_mul_pow for the existence of such a representation.

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. See quo_mul_prod_add_sum_rem_mul_prod_unique for the uniqueness of this representation.

theorem Polynomial.quo_mul_prod_add_sum_rem_mul_prod_unique {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {g : ι → Polynomial R} (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) {q₁ q₂ : Polynomial R} {r₁ r₂ : ι → Polynomial R} (hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree) (hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree) (hf : q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k = q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k) : 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. Then f can be written in the form (∏ i ∈ s, g i) * (q + ∑ i ∈ s, r i / g i) in at most one way, where degree (r i) < degree (g i) and the denominator cancels formally. See eq_quo_mul_prod_add_sum_rem_mul_prod for the existence of such a representation.

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. See quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique for the uniqueness of this representation.

theorem Polynomial.quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {g : ι → Polynomial R} (hg : ∀ i ∈ s, (g i).Monic) (hgg : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) {n : ι → ℕ} {q₁ q₂ : Polynomial R} {r₁ r₂ : (i : ι) → Fin (n i) → Polynomial R} (hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree) (hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree) (hf : 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 = 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) : 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. 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)) in at most one way, where degree (r i j) < degree (g i) and the denominator cancels formally. See eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow for the existence of such a representation.

theorem Polynomial.mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse {R : Type u_1} [CommRing R] {K : Type u_2} [CommRing K] [Algebra (Polynomial R) K] [Nontrivial R] {ι : 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). See mul_prod_pow_inverse_eq_quo_add_sum_rem_mul_pow_inverse for the uniqueness of this representation.

theorem Polynomial.quo_add_sum_rem_mul_pow_inverse_unique {R : Type u_1} [CommRing R] {K : Type u_2} [CommRing K] [Algebra (Polynomial R) K] [FaithfulSMul (Polynomial R) K] {ι : Type u_3} {s : Finset ι} {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₁ q₂ : Polynomial R} {r₁ r₂ : (i : ι) → Fin (n i) → Polynomial R} (hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree) (hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree) (hf : (algebraMap (Polynomial R) K) q₁ + ∑ i ∈ s, ∑ j : Fin (n i), (algebraMap (Polynomial R) K) (r₁ i j) * gi i ^ (↑j + 1) = (algebraMap (Polynomial R) K) q₂ + ∑ i ∈ s, ∑ j : Fin (n i), (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.

theorem Polynomial.div_prod_eq_quo_add_sum_rem_div {R : Type u_1} [CommRing 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. See quo_add_sum_rem_div_unique for the uniqueness of this representation.

@[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] (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. See quo_add_sum_rem_div_unique for the uniqueness of this representation.

theorem Polynomial.quo_add_sum_rem_div_unique {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra (Polynomial R) K] [FaithfulSMul (Polynomial R) K] {ι : 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₁ q₂ : Polynomial R} {r₁ r₂ : ι → Polynomial R} (hr₁ : ∀ i ∈ s, (r₁ i).degree < (g i).degree) (hr₂ : ∀ i ∈ s, (r₂ i).degree < (g i).degree) (hf : ↑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.

theorem Polynomial.div_eq_quo_add_rem_div_add_rem_div {R : Type u_1} [CommRing 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]. See quo_add_rem_div_add_rem_div_unique for the uniqueness of this representation.

@[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] (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]. See quo_add_rem_div_add_rem_div_unique for the uniqueness of this representation.

theorem Polynomial.quo_add_rem_div_add_rem_div_unique {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra (Polynomial R) K] [FaithfulSMul (Polynomial R) K] {g₁ g₂ : Polynomial R} (hg₁ : g₁.Monic) (hg₂ : g₂.Monic) (hcoprime : IsCoprime g₁ g₂) {q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : Polynomial R} (hr₁₁ : r₁₁.degree < g₁.degree) (hr₁₂ : r₁₂.degree < g₁.degree) (hr₂₁ : r₂₁.degree < g₂.degree) (hr₂₂ : r₂₂.degree < g₂.degree) (hf : ↑q₁ + ↑r₁₁ / ↑g₁ + ↑r₂₁ / ↑g₂ = ↑q₂ + ↑r₁₂ / ↑g₁ + ↑r₂₂ / ↑g₂) : q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Let R be an integral domain and f, g₁, g₂ : R[X]. Let g₁ and g₂ be monic and coprime. Then the representation of f / (g₁ * g₂) as q + r₁ / g₁ + r₂ / g₂ for q r₁ r₂ : R[X] and degree rᵢ < degree gᵢ is unique, where the equality is taken in a field K containing R[X]. See div_eq_quo_add_rem_div_add_rem_div for the existence of such a representation.