Documentation

Mathlib.Data.Polynomial.PartialFractions

Partial fractions #

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

The main theorem #

Scope for Expansion #

theorem div_eq_quo_add_rem_div_add_rem_div (R : Type) [CommRing R] [IsDomain R] (K : Type) [Field K] [Algebra (Polynomial R) K] [IsFractionRing (Polynomial R) K] (f : Polynomial R) {g₁ : Polynomial R} {g₂ : Polynomial R} (hg₁ : Polynomial.Monic g₁) (hg₂ : Polynomial.Monic g₂) (hcoprime : IsCoprime g₁ g₂) :
∃ (q : Polynomial R) (r₁ : Polynomial R) (r₂ : Polynomial R), Polynomial.degree r₁ < Polynomial.degree g₁ Polynomial.degree r₂ < Polynomial.degree g₂ 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 deg(r₁) < deg(g₁) and deg(r₂) < deg(g₂).

theorem div_eq_quo_add_sum_rem_div (R : Type) [CommRing R] [IsDomain R] (K : Type) [Field K] [Algebra (Polynomial R) K] [IsFractionRing (Polynomial R) K] (f : Polynomial R) {ι : Type u_1} {g : ιPolynomial R} {s : Finset ι} (hg : is, Polynomial.Monic (g i)) (hcop : Set.Pairwise s fun (i j : ι) => IsCoprime (g i) (g j)) :
∃ (q : Polynomial R) (r : ιPolynomial R), (is, Polynomial.degree (r i) < Polynomial.degree (g i)) (f / Finset.prod s fun (i : ι) => (g i)) = q + Finset.sum s fun (i : ι) => (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 / ∏ (g i) can be rewritten as q + ∑ (r i) / (g i), where deg(r i) < deg(g i), provided that the g i are monic and pairwise coprime.