mathlib3 documentation


Partial fractions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) [comm_ring R] [is_domain R] (K : Type) [field K] [algebra (polynomial R) K] [is_fraction_ring (polynomial R) K] (f : polynomial R) {g₁ g₂ : polynomial R} (hg₁ : g₁.monic) (hg₂ : g₂.monic) (hcoprime : is_coprime g₁ g₂) :
(q 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) [comm_ring R] [is_domain R] (K : Type) [field K] [algebra (polynomial R) K] [is_fraction_ring (polynomial R) K] (f : polynomial R) {ι : Type u_1} {g : ι polynomial R} {s : finset ι} (hg : (i : ι), i s (g i).monic) (hcop : s.pairwise (λ (i j : ι), is_coprime (g i) (g j))) :
(q : polynomial R) (r : ι polynomial R), ( (i : ι), i s (r i).degree < (g i).degree) f / (λ (i : ι), (g i)) = q + s.sum (λ (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.