Documentation

Mathlib.Algebra.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₁ : 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 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, (g i).Monic) (hcop : (↑s).Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) :
∃ (q : Polynomial R) (r : ιPolynomial R), (∀ is, (r i).degree < (g i).degree) f / is, (g i) = q + is, (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.