Polynomial.dvd_iff_modByMonic_eq_zero
theorem Polynomial.dvd_iff_modByMonic_eq_zero :
∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, q.Monic → (p.modByMonic q = 0 ↔ q ∣ p)
This theorem, named `Polynomial.dvd_iff_modByMonic_eq_zero`, states that for any type `R` that is a ring, and for any polynomials `p` and `q` over `R`, if `q` is a monic polynomial, then `p` mod `q` equals to zero if and only if `q` divides `p`. Here, a polynomial is considered monic if its leading coefficient is 1 (`Polynomial.Monic`). The symbol `%ₘ` represents the modulo operation in the context of polynomials, and `∣` denotes polynomial division.
More concisely: For any ring `R`, polynomial `p`, and monic polynomial `q` over `R`, `p %ₘ q = 0` if and only if `q` divides `p`.
|
Polynomial.multiplicity_X_sub_C_finite
theorem Polynomial.multiplicity_X_sub_C_finite :
∀ {R : Type u} [inst : Ring R] {p : Polynomial R} (a : R),
p ≠ 0 → multiplicity.Finite (Polynomial.X - Polynomial.C a) p
This theorem states that for any non-zero polynomial `p` over a ring `R` and any element `a` in `R`, the multiplicity of the polynomial `X - C(a)` in `p` is finite. In other words, there exists a natural number `n` such that `(X - C(a))^(n + 1)` does not divide `p`. Here, `X` represents the polynomial variable and `C(a)` is the constant polynomial `a`.
More concisely: For any non-zero polynomial `p` over a ring `R` and any `a` in `R`, there exists a natural number `n` such that `(X - a)^(n + 1)` does not divide `p`.
|
Polynomial.rootMultiplicity_eq_zero
theorem Polynomial.rootMultiplicity_eq_zero :
∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {x : R}, ¬p.IsRoot x → Polynomial.rootMultiplicity x p = 0
The theorem `Polynomial.rootMultiplicity_eq_zero` states that for any commutative ring `R`, any polynomial `p` of `R`, and any element `x` of `R`, if `x` is not a root of the polynomial `p` (meaning that when `x` is substituted into `p`, the result is not zero), then the root multiplicity of `x` in `p` is zero. In other words, the term `X - C x` does not divide `p`.
More concisely: If an element `x` in a commutative ring `R` is not a root of polynomial `p` in `R`, then the multiplicity of `x` as a root of `p` is zero.
|
Polynomial.rootMultiplicity_zero
theorem Polynomial.rootMultiplicity_zero :
∀ {R : Type u} [inst : Ring R] {x : R}, Polynomial.rootMultiplicity x 0 = 0
This theorem states that for any ring `R` and any element `x` of `R`, the root multiplicity of `x` in the zero polynomial is zero. In other words, no value is a root of the zero polynomial in a ring, or equivalently, the zero polynomial has no roots, hence its root multiplicity is zero for every element of the ring.
More concisely: The zero polynomial has no roots in any ring, hence its root multiplicity for every element is zero.
|
Polynomial.rootMultiplicity_eq_multiplicity
theorem Polynomial.rootMultiplicity_eq_multiplicity :
∀ {R : Type u} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : DecidableRel fun x x_1 => x ∣ x_1]
(p : Polynomial R) (a : R),
Polynomial.rootMultiplicity a p =
if h0 : p = 0 then 0 else (multiplicity (Polynomial.X - Polynomial.C a) p).get ⋯
This theorem states that for any ring `R` with decidable equality and a decidable relation for divisibility, given a polynomial `p` and an element `a` of `R`, the root multiplicity of `a` in `p` is equal to the multiplicity of the polynomial `X - C a` in `p`. In other words, the root multiplicity of `a` in `p` is the largest power of `X - C a` that divides `p`. If `p` is the zero polynomial, the root multiplicity is defined to be zero. The multiplicity is computed with respect to the PartENat number system, which includes natural numbers and an infinity element.
More concisely: For any ring with decidable equality and a decidable divisibility relation, the root multiplicity of an element in a polynomial is equal to the multiplicity of the corresponding linear polynomial in the given polynomial.
|
Polynomial.divByMonic_eq_zero_iff
theorem Polynomial.divByMonic_eq_zero_iff :
∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} [inst_1 : Nontrivial R],
q.Monic → (p.divByMonic q = 0 ↔ p.degree < q.degree)
The theorem `Polynomial.divByMonic_eq_zero_iff` states that for any ring `R`, given two polynomials `p` and `q` from `R` and assuming `R` is nontrivial, if `q` is monic (meaning its leading coefficient is 1), then the result of the division of `p` by `q` is zero if and only if the degree of `p` is less than the degree of `q`. In other words, a polynomial `p` divided by a monic polynomial `q` equals zero precisely when `p` has a lower degree than `q`.
More concisely: For a nontrivial ring R and monic polynomials p and q of degrees d(p) and d(q) respectively, p / q = 0 if and only if d(p) < d(q).
|
Polynomial.degree_modByMonic_lt
theorem Polynomial.degree_modByMonic_lt :
∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] (p : Polynomial R) {q : Polynomial R},
q.Monic → (p.modByMonic q).degree < q.degree
This theorem states that for any given type `R` that constitutes a ring and is nontrivial, and for any two polynomials `p` and `q` of type `R`, if `q` is a monic polynomial (meaning its leading coefficient is 1), then the degree of the polynomial obtained by taking the modulo of `p` by `q` is strictly less than the degree of `q`.
In mathematical terms, if `p` and `q` are polynomials over a nontrivial ring, and `q` is monic, then the degree of `p mod q` is less than the degree of `q`.
More concisely: For any nontrivial ring `R`, if `p` and `q` are polynomials over `R` with `q` monic, then the degree of `p` modulo `q` is strictly less than the degree of `q`.
|
Polynomial.modByMonic_eq_sub_mul_div
theorem Polynomial.modByMonic_eq_sub_mul_div :
∀ {R : Type u} [inst : Ring R] (p : Polynomial R) {q : Polynomial R},
q.Monic → p.modByMonic q = p - q * p.divByMonic q
The theorem `Polynomial.modByMonic_eq_sub_mul_div` is a statement about polynomials over a ring. It states that for any given ring `R` and any polynomials `p` and `q` in that ring, if the polynomial `q` is Monic (i.e., its leading coefficient is 1), then the remainder of `p` divided by `q` (denoted as `p %ₘ q`) is equal to the difference between `p` and the product of `q` and the quotient of `p` divided by `q` (denoted as `p - q * (p /ₘ q)`). In essence, this theorem is a mathematical expression of the division algorithm for polynomials where the divisor is a monic polynomial.
More concisely: For any polynomials `p` and `q` in a ring where `q` is monic, `p %ₘ q` equals `p - q * (p /ₘ q)`.
|
Polynomial.modByMonic_add_div
theorem Polynomial.modByMonic_add_div :
∀ {R : Type u} [inst : Ring R] (p : Polynomial R) {q : Polynomial R},
q.Monic → p.modByMonic q + q * p.divByMonic q = p
The theorem `Polynomial.modByMonic_add_div` states that for any type `R` that is a ring, for any polynomial `p` and any monic polynomial `q` (a polynomial is considered monic if its leading coefficient is 1), the sum of the remainder of `p` divided by `q` and the result of `q` multiplied by the quotient of `p` divided by `q` is equal to `p`. In other words, this is the polynomial version of the division algorithm, where the quotient and remainder satisfy the equation `p = q * quotient + remainder`.
More concisely: For any ring type `R`, monic polynomial `q(X)` and polynomial `p(X)` over `R`, we have `p = q * (p divide q) + remainder(p divide q)`, where `p divide q` is the quotient and `remainder(p divide q)` is the remainder of `p` divided by `q`.
|
Polynomial.map_dvd_map
theorem Polynomial.map_dvd_map :
∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
Function.Injective ⇑f → ∀ {x y : Polynomial R}, x.Monic → (Polynomial.map f x ∣ Polynomial.map f y ↔ x ∣ y)
The theorem `Polynomial.map_dvd_map` states that for any two types `R` and `S` with ring structure, any ring homomorphism `f` from `R` to `S`, and for any two polynomials `x` and `y` over `R`, if `f` is injective and `x` is a monic polynomial, then `x` divides `y` if and only if the image of `x` under `f` divides the image of `y` under `f`. Here, a polynomial is said to divide another if there exists a third polynomial which multiplied by the first gives the second. The mapping of a polynomial `p` across a ring hom `f` is performed using the `Polynomial.map` function.
More concisely: For any injective ring homomorphism `f` between rings `R` and `S` and monic polynomials `x` and `y` over `R`, `x` divides `y` if and only if the image of `x` under `f` divides the image of `y` under `f` in `S`.
|
Polynomial.mul_divByMonic_eq_iff_isRoot
theorem Polynomial.mul_divByMonic_eq_iff_isRoot :
∀ {R : Type u} {a : R} [inst : CommRing R] {p : Polynomial R},
(Polynomial.X - Polynomial.C a) * p.divByMonic (Polynomial.X - Polynomial.C a) = p ↔ p.IsRoot a
This theorem states that for any commutative ring `R`, any element `a` of `R`, and any polynomial `p` over `R`, the polynomial `p` is equal to the product of `(Polynomial.X - Polynomial.C a)` and the result of dividing `p` by `(Polynomial.X - Polynomial.C a)` if and only if `a` is a root of the polynomial `p`. In terms of mathematics, this is saying that for a polynomial $p(x)$ and a number $a$, $p(x) = (x-a)q(x)$ if and only if $p(a) = 0$, where $q(x)$ is the quotient when $p(x)$ is divided by $(x-a)$.
More concisely: A polynomial `p` over a commutative ring `R` has a root `a` in `R` if and only if `p` equals the product of `(X - Polynomial.C a)` and the quotient of `p` by `(X - Polynomial.C a)`, where `X` is an indeterminate over `R`.
|
Polynomial.div_modByMonic_unique
theorem Polynomial.div_modByMonic_unique :
∀ {R : Type u} [inst : Ring R] {f g : Polynomial R} (q r : Polynomial R),
g.Monic → r + g * q = f ∧ r.degree < g.degree → f.divByMonic g = q ∧ f.modByMonic g = r
The theorem `Polynomial.div_modByMonic_unique` states that for any ring `R` and any polynomials `f`, `g`, `q`, and `r` over `R`, if `g` is a monic polynomial (that is, its leading coefficient is 1), and `r` plus `g` times `q` equals `f` with the degree of `r` being less than the degree of `g`, then the quotient of `f` divided by `g` (using monic division) is `q` and the remainder of `f` divided by `g` (also using monic division) is `r`. This theorem sets a unique condition for the division and remainder calculation in the context of monic polynomials.
More concisely: If `f`, `g` are polynomials over a ring `R` with `g` monic and of higher degree than `r`, then the quotient of `f` divided by `g` is `q` and the remainder of `f` divided by `g` is `r` if and only if `r` is the remainder of `f` when divided by `g` using monic division.
|
Polynomial.dvd_iff_isRoot
theorem Polynomial.dvd_iff_isRoot :
∀ {R : Type u} {a : R} [inst : CommRing R] {p : Polynomial R}, Polynomial.X - Polynomial.C a ∣ p ↔ p.IsRoot a := by
sorry
The theorem `Polynomial.dvd_iff_isRoot` states that for any commutative ring `R`, an element `a` from `R`, and a polynomial `p` of coefficients from `R`, the polynomial `X - C a` (where `X` is the polynomial variable and `C a` is the constant polynomial `a`) divides `p` if and only if `a` is a root of `p`. In mathematical terms, \(x - a\) divides a polynomial \(p(x)\) if and only if \(a\) is a root of \(p(x)\) which means that the polynomial evaluated at \(a\) is zero.
More concisely: For any commutative ring R, polynomial p, and element a from R, the polynomial X - a divides p if and only if a is a root of p, i.e., p(a) = 0.
|
Polynomial.modByMonic_X_sub_C_eq_C_eval
theorem Polynomial.modByMonic_X_sub_C_eq_C_eval :
∀ {R : Type u} [inst : CommRing R] (p : Polynomial R) (a : R),
p.modByMonic (Polynomial.X - Polynomial.C a) = Polynomial.C (Polynomial.eval a p)
The theorem `Polynomial.modByMonic_X_sub_C_eq_C_eval` states that for any commutative ring `R`, any polynomial `p` over `R`, and any element `a` of `R`, the remainder of `p` when divided by the polynomial `X - C a` (where `X` is the polynomial variable and `C a` is the constant polynomial `a`) is equal to the constant polynomial whose coefficient is the value of `p` evaluated at `a`. In mathematical terms, this can be written as `p mod (X - a) = C(p(a))` for any polynomial `p` and any `a` in a commutative ring.
More concisely: For any commutative ring R, polynomial p over R, and its element a, the remainder of p divided by X - Ca equals the constant polynomial with coefficient p(a).
|
Polynomial.pow_rootMultiplicity_dvd
theorem Polynomial.pow_rootMultiplicity_dvd :
∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (a : R),
(Polynomial.X - Polynomial.C a) ^ Polynomial.rootMultiplicity a p ∣ p
The theorem `Polynomial.pow_rootMultiplicity_dvd` states that for every polynomial `p` over a ring `R` and for every element `a` in `R`, the polynomial `(Polynomial.X - Polynomial.C a)` raised to the power of the root multiplicity of `a` in `p` divides `p`. In mathematical terms, if `a` is a root of `p` and its multiplicity is `n`, then `(X - a)^n` is a factor of `p`.
More concisely: For any polynomial `p` over a ring `R` and any root `a` of `p` with multiplicity `n`, `(X - a)^n` divides `p` in `R[X]`.
|
Polynomial.zero_divByMonic
theorem Polynomial.zero_divByMonic : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), 0 /ₘ p = 0
This theorem states that for all types `R`, which are instances of the Ring structure, and any polynomial `p` of `R`, the division of the zero polynomial by `p` is equal to the zero polynomial. In other words, it's stating that dividing zero by any polynomial yields zero, in the context of polynomial rings.
More concisely: For all rings R and polynomials p in R, 0 / p = 0.
|
Polynomial.degree_add_divByMonic
theorem Polynomial.degree_add_divByMonic :
∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
q.Monic → q.degree ≤ p.degree → q.degree + (p.divByMonic q).degree = p.degree
The theorem `Polynomial.degree_add_divByMonic` states that for any ring `R` and any polynomials `p` and `q` over `R`, if `q` is monic (its leading coefficient is 1) and the degree of `q` is less than or equal to the degree of `p`, then the sum of the degree of `q` and the degree of the quotient of `p` divided by `q` (`p /ₘ q`) equals the degree of `p`. Essentially, this theorem captures the relationship between the degrees of two polynomials and their quotient in certain conditions.
More concisely: For any ring R and monic polynomial q of degree less than or equal to that of polynomial p over R, the degree of p equals the degree of q plus the degree of the quotient p /ₘ q.
|