div_eq_quo_add_sum_rem_div
theorem div_eq_quo_add_sum_rem_div :
∀ (R : Type) [inst : CommRing R] [inst_1 : IsDomain R] (K : Type) [inst_2 : Field K]
[inst_3 : Algebra (Polynomial R) K] [inst_4 : IsFractionRing (Polynomial R) K] (f : Polynomial R) {ι : Type u_1}
{g : ι → Polynomial R} {s : Finset ι},
(∀ i ∈ s, (g i).Monic) →
((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
∃ q r,
(∀ i ∈ s, (r i).degree < (g i).degree) ∧
(↑f / s.prod fun i => ↑(g i)) = ↑q + s.sum fun i => ↑(r i) / ↑(g i)
The theorem states that given an integral domain `R` and a polynomial `f` from `R`, along with a finite index set `s`. If we consider a fraction form of `f` divided by the product of polynomials `g i` (for each `i` in `s`), then it can be rewritten as a sum of `q` and the sum of `r i` divided by `g i` (for each `i` in `s`), where the degree of `r i` is less than the degree of `g i`. This is under the condition that each `g i` is monic and pairwise coprime. This result is a generalization of the Euclidean division algorithm to polynomials.
More concisely: Given an integral domain `R`, a monic polynomial `f` from `R`, and a finite index set `s` of pairwise coprime monic polynomials `g_i` from `R`, there exist polynomials `q` and `r_i` in `R` such that `f = q * (∏ g_i) + ∑ (r_i / g_i)`, where the degree of each `r_i` is less than the degree of `g_i`.
|
div_eq_quo_add_rem_div_add_rem_div
theorem div_eq_quo_add_rem_div_add_rem_div :
∀ (R : Type) [inst : CommRing R] [inst_1 : IsDomain R] (K : Type) [inst_2 : Field K]
[inst_3 : Algebra (Polynomial R) K] [inst_4 : IsFractionRing (Polynomial R) K] (f : Polynomial R)
{g₁ g₂ : Polynomial R},
g₁.Monic →
g₂.Monic →
IsCoprime g₁ g₂ →
∃ q r₁ r₂, r₁.degree < g₁.degree ∧ r₂.degree < g₂.degree ∧ ↑f / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂
This theorem states that given an integral domain `R` and a field of fractions `K` of polynomials over `R`, and given three polynomials `f`, `g₁`, and `g₂` over `R` such that `g₁` and `g₂` are monic and coprime, there exist polynomials `q`, `r₁`, and `r₂` such that the degree of `r₁` is less than the degree of `g₁`, the degree of `r₂` is less than the degree of `g₂`, and the fraction of `f` over the product of `g₁` and `g₂` can be expressed as the sum of `q` and the fractions of `r₁` and `r₂` over `g₁` and `g₂`, respectively. The theorem essentially provides a polynomial division rule in the ring of polynomials when the divisor is a product of two coprime monic polynomials.
More concisely: Given an integral domain `R`, a field of fractions `K` of polynomials over `R`, and two monic coprime polynomials `g₁` and `g₂` over `R`, there exist polynomials `q`, `r₁`, and `r₂` such that `f = q * (g₁ * g₂) + r₁ * g₁ + r₂ * g₂` where the degrees of `r₁` and `r₂` are less than the degrees of `g₁` and `g₂`, respectively.
|