Polynomial.mem_roots'
theorem Polynomial.mem_roots' :
∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a
The theorem `Polynomial.mem_roots'` states that for any type `R`, any instance `a` of type `R`, and any polynomial `p` of type `Polynomial R`, `a` is a root of `p` (i.e., is in the multiset of roots of `p` denoted by `Polynomial.roots p`) if and only if two conditions hold: the polynomial `p` is not the zero polynomial (`p ≠ 0`) and `a` is indeed a root of `p` (denoted by `Polynomial.IsRoot p a` which means the evaluation of `p` at `a` equals zero). Here, `R` is assumed to be a commutative ring and also an integral domain.
More concisely: For any commutative ring and integral domain R, an element a of R is a root of a non-zero polynomial p in R if and only if a is in the multiset of roots of p.
|
Polynomial.rootMultiplicity_X_sub_C_pow
theorem Polynomial.rootMultiplicity_X_sub_C_pow :
∀ {R : Type u} [inst : CommRing R] [inst_1 : Nontrivial R] (a : R) (n : ℕ),
Polynomial.rootMultiplicity a ((Polynomial.X - Polynomial.C a) ^ n) = n
This theorem states that in the context of a commutative ring `R` that is nontrivial, for any element `a` of `R` and any natural number `n`, the multiplicity of `a` as a root of the polynomial `(X - a) ^ n` is `n`. In simpler terms, it says that the polynomial `(X - a) ^ n` has `a` as a root `n` times. Here, `X` represents the polynomial variable, `a` is a constant, and `n` is the power to which the polynomial is raised. The multiplicity of a root of a polynomial is the number of times the root appears--in this case, `n` times.
More concisely: In a commutative nontrivial ring, for any element `a` and natural number `n`, the polynomial `(X - a) ^ n` has `a` as a root of multiplicity `n`.
|
Polynomial.degree_le_of_dvd
theorem Polynomial.degree_le_of_dvd :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p q : Polynomial R},
p ∣ q → q ≠ 0 → p.degree ≤ q.degree
The theorem `Polynomial.degree_le_of_dvd` states that for any type `R` with a semiring structure and no zero divisors, and for any two polynomials `p` and `q` over `R`, if `p` divides `q` and `q` is not the zero polynomial, then the degree of `p` is less than or equal to the degree of `q`. In other words, if one polynomial divides another, the degree of the divisor polynomial cannot exceed the degree of the dividend polynomial, provided that the dividend polynomial is not zero.
More concisely: If `p` divides `q` in a semiring `R` without zero divisors, then the degree of `p` is less than or equal to the degree of `q`.
|
Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C
theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
Multiset.card p.roots = p.natDegree →
Polynomial.C p.leadingCoeff * (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
The theorem `Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C` states that for any polynomial `p` over a commutative ring `R` (which is assumed to be an integral domain), if the number of roots of `p` (counting multiplicities) equals the degree of `p` (in natural numbers), then `p` can be expressed as the product of its leading coefficient and the product of linear terms `(X - a)` where `a` varies over the roots of `p`. In other words, if a polynomial has as many roots as its degree, it can be factored into linear terms multiplied by its leading coefficient. In mathematical terms, this can be written as $p = p.\text{leadingCoeff} \times \prod (X - a)$, where $a$ ranges over the roots of $p$.
More concisely: If a polynomial of degree n over a commutative integral domain has exactly n roots (counting multiplicities), then it can be expressed as the product of its leading coefficient and the product of linear factors (X - a) over its roots a.
|
Polynomial.degree_coe_units
theorem Polynomial.degree_coe_units :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] [inst_2 : Nontrivial R] (u : (Polynomial R)ˣ),
(↑u).degree = 0
The theorem `Polynomial.degree_coe_units` states that for any type `R` that is a semiring, has no zero divisors, and is nontrivial, the degree of any unit `u` in the unit group of the polynomial ring over `R`, when considered as a polynomial itself, is always zero. In other words, if we have a unit in the polynomial ring, it must be a constant polynomial, as only constant polynomials have a degree of zero.
More concisely: In a semiring without zero divisors and of positive size, every unit in the polynomial ring over it is a constant polynomial of degree 0.
|
Polynomial.roots_pow
theorem Polynomial.roots_pow :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R) (n : ℕ), (p ^ n).roots = n • p.roots
The theorem `Polynomial.roots_pow` states that for any polynomial `p` over a domain `R` which forms a commutative ring, and any natural number `n`, the roots of `p` raised to the power `n` are the same as `n` times the roots of `p`. This means that taking a polynomial to a power `n` doesn't change its set of roots, but instead each root's multiplicity is multiplied by `n`.
More concisely: For any polynomial `p` over a commutative ring `R` and natural number `n`, the roots of `p` are the same as the roots of `p^n`, each with multiplicity multiplied by `n`.
|
Polynomial.natDegree_sub_eq_of_prod_eq
theorem Polynomial.natDegree_sub_eq_of_prod_eq :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p₁ p₂ q₁ q₂ : Polynomial R},
p₁ ≠ 0 →
q₁ ≠ 0 → p₂ ≠ 0 → q₂ ≠ 0 → p₁ * q₂ = p₂ * q₁ → ↑p₁.natDegree - ↑q₁.natDegree = ↑p₂.natDegree - ↑q₂.natDegree
This theorem states that for any type `R` with a semiring structure and no zero divisors, and for any non-zero polynomials `p₁`, `p₂`, `q₁`, and `q₂` over `R`, if `p₁ * q₂` equals `p₂ * q₁`, then the difference between the 'natural degree' of `p₁` and `q₁` (i.e., `Polynomial.natDegree p₁ - Polynomial.natDegree q₁`) is equal to the difference between the 'natural degree' of `p₂` and `q₂` (i.e., `Polynomial.natDegree p₂ - Polynomial.natDegree q₂`).
Here, the 'natural degree' of a polynomial is a concept that generalizes the degree of a polynomial. For the zero polynomial, its 'natural degree' is defined to be zero. For a non-zero polynomial, its 'natural degree' is the degree of the polynomial.
More concisely: For polynomials $p\_1, p\_2, q\_1,$ and $q\_2$ over a semiring $R$ without zero divisors, if $p\_1 \cdot q\_2 = p\_2 \cdot q\_1$, then $\text{deg}(p\_1) - \text{deg}(q\_1) = \text{deg}(p\_2) - \text{deg}(q\_2)$, where $\text{deg}$ denotes the natural degree.
|
Polynomial.mem_nthRoots
theorem Polynomial.mem_nthRoots :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ},
0 < n → ∀ {a x : R}, x ∈ Polynomial.nthRoots n a ↔ x ^ n = a
The theorem `Polynomial.mem_nthRoots` states that for any commutative ring `R` that is also a domain, any natural number `n` that is greater than zero, and any elements `a` and `x` from `R`, `x` is a solution to the equation `x^n = a` if and only if `x` is in the multiset of `n`-th roots of `a`. In other words, it provides a characterization of the `n`-th roots of `a` in terms of the solutions to the polynomial equation `x^n = a`.
More concisely: For any commutative domain R, natural number n > 0, and elements a and x in R, x is an n-th root of a if and only if x is a solution to the equation x^n = a.
|
Polynomial.roots_one
theorem Polynomial.roots_one : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.roots 1 = ∅ := by
sorry
This theorem states that for any type `R` which is a commutative ring and an integral domain, the roots of the polynomial `1` are an empty multiset, denoted by `∅`. In other words, the polynomial `1` has no roots in this domain.
More concisely: For any commutative ring and integral domain R, the polynomial 1 has no roots in R.
|
Polynomial.natDegree_mul
theorem Polynomial.natDegree_mul :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p q : Polynomial R},
p ≠ 0 → q ≠ 0 → (p * q).natDegree = p.natDegree + q.natDegree
This theorem states that for any semiring `R` with no zero divisors, and for any two non-zero polynomials `p` and `q` from `R`, the natural degree of the product of `p` and `q` is equal to the sum of the natural degrees of `p` and `q`. In other words, the degree of a product of two non-zero polynomials is the sum of the degrees of the polynomials. This mirrors the familiar property from algebra where the degree of the product of two non-zero polynomials is the sum of their degrees.
More concisely: Given a semiring `R` without zero divisors, the degree of the product of two non-zero polynomials `p` and `q` from `R` equals the sum of the degrees of `p` and `q`.
|
Polynomial.rootMultiplicity_le_iff
theorem Polynomial.rootMultiplicity_le_iff :
∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
p ≠ 0 → ∀ (a : R) (n : ℕ), Polynomial.rootMultiplicity a p ≤ n ↔ ¬(Polynomial.X - Polynomial.C a) ^ (n + 1) ∣ p
This theorem states that for any commutative ring `R`, and any non-zero polynomial `p` with coefficients in `R`, for any element `a` of `R` and natural number `n`, the root multiplicity of `a` in `p` is less than or equal to `n` if and only if the polynomial `(X - C a)` to the power `(n + 1)` does not divide `p`. Here, `X` denotes the polynomial variable and `C a` is the constant polynomial `a`. In other words, the theorem provides a condition to check whether the root multiplicity of a certain value in a polynomial is less than or equal to a given natural number.
More concisely: For any commutative ring R, polynomial p with non-zero leading coefficient, and element a in R, the root multiplicity of a in p is less than or equal to n if and only if (X - a)^(n+1) does not divide p.
|
Polynomial.finite_setOf_isRoot
theorem Polynomial.finite_setOf_isRoot :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, p ≠ 0 → {x | p.IsRoot x}.Finite := by
sorry
This theorem states that for any commutative ring `R` which is also an integral domain, and for any non-zero polynomial `p` over `R`, the set of roots of `p` (i.e., the set of elements `x` in `R` such that `p` evaluated at `x` equals 0) is finite. In other words, a non-zero polynomial over an integral domain has only finitely many roots.
More concisely: In an integral domain, a non-zero polynomial has finitely many roots.
|
Polynomial.degree_pos_of_not_isUnit_of_dvd_monic
theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic :
∀ {R : Type u} [inst : CommSemiring R] {a p : Polynomial R}, ¬IsUnit a → a ∣ p → p.Monic → 0 < a.degree
This theorem states that for a commutative semiring `R` and two polynomials `a` and `p` over `R`, if `a` is not a unit and `a` divides `p`, and if `p` is a monic polynomial (its leading coefficient is 1), then the degree of `a` is positive. In other words, if a non-unit polynomial `a` divides a monic polynomial `p`, then `a` must be of degree greater than zero.
More concisely: If `a` is a non-unit polynomial of degree 0 in a commutative semiring `R`, `a` does not divide a monic polynomial `p` in `R`.
|
Polynomial.nthRootsFinset_zero
theorem Polynomial.nthRootsFinset_zero :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.nthRootsFinset 0 R = ∅
The theorem `Polynomial.nthRootsFinset_zero` states that for any commutative ring `R` that is also an integral domain, the set of zeroth roots of unity in `R` is the empty set. In other words, there are no elements in `R` that satisfy the equation `x^0 = 1` where `x` is an element in `R`, except the case where `0 = 0`.
More concisely: In an integral domain, there are no non-zero zeroth roots of unity.
|
Polynomial.card_roots'
theorem Polynomial.card_roots' :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R), Multiset.card p.roots ≤ p.natDegree
The theorem `Polynomial.card_roots'` states that for any polynomial `p` over a type `R` that is a commutative ring and an integral domain, the cardinality (or number of elements considering their multiplicities) of the multiset of roots of `p` is less than or equal to the natural degree of `p`. The natural degree of a polynomial is the degree of the polynomial treated as a natural number, with the degree of the zero polynomial defined as 0.
More concisely: The number of roots (counting multiplicities) of a polynomial over a commutative ring and integral domain does not exceed its degree.
|
Polynomial.degree_eq_one_of_irreducible_of_root
theorem Polynomial.degree_eq_one_of_irreducible_of_root :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
Irreducible p → ∀ {x : R}, p.IsRoot x → p.degree = 1
This theorem states that for any commutative ring `R`, which is also an integral domain, and for any irreducible polynomial `p` over `R`, if `x` is a root of `p`, then the degree of `p` must be equal to 1. In other words, if a polynomial is irreducible (cannot be factored into polynomials of lower degree) and has a root in the ring, then it must be a linear polynomial.
More concisely: For any commutative ring that is an integral domain and any irreducible polynomial of degree greater than 1 over it, it has no roots.
|
Polynomial.mem_rootSet_of_ne
theorem Polynomial.mem_rootSet_of_ne :
∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra T S] [inst_4 : NoZeroSMulDivisors T S],
p ≠ 0 → ∀ {a : S}, a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0
This theorem states that for any commutative ring `T` and a polynomial `p` over `T`, any type `S` that is a commutative ring, a domain, and an algebra over `T` with no zero `T`-`S` mul divisors, if the polynomial `p` is not the zero polynomial, then a member `a` of type `S` is in the set of distinct roots of `p` in `S` (i.e., `Polynomial.rootSet p S`) if and only if applying the algebra homomorphism given by evaluating the polynomial `p` at `a` (i.e., `(Polynomial.aeval a) p`) results in zero. This theorem essentially describes the condition for an element to be a root of a polynomial in the context of algebraic structures.
More concisely: For a commutative ring `T`, a polynomial `p` over `T`, a commutative ring and domain `S` an algebra over `T`, and an element `a` in `S` with no zero `T-S` multiplicative divisors, `a` is a root of `p` in `S` if and only if evaluating `p` at `a` results in zero.
|
Polynomial.roots_X_sub_C
theorem Polynomial.roots_X_sub_C :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (r : R), (Polynomial.X - Polynomial.C r).roots = {r} := by
sorry
This theorem states that for any commutative ring `R`, which is also an integral domain, and any element `r` from `R`, the roots of the polynomial `X - r` is a multiset containing only the element `r`. In mathematical terms, if `R` is a commutative ring and `r` is an element of `R`, then the root of the polynomial `X - r` is exactly `r`. This is consistent with the well-known fact from algebra that the root of a linear polynomial `X - a` is `a`.
More concisely: For any commutative ring `R` being an integral domain and any `r` in `R`, the polynomial `X - r` has exactly the root `r`.
|
Polynomial.prod_multiset_X_sub_C_dvd
theorem Polynomial.prod_multiset_X_sub_C_dvd :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R),
(Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod ∣ p
This theorem states that for any polynomial `p` over a commutative ring `R` that is also an integral domain, the polynomial obtained by taking the product of terms `(X - a)` for each `a` in the set of roots of `p` (each root `a` appearing as many times as its multiplicity in `p`), divides `p`. In other words, `p` is a multiple of the product of its linear factors. Using LaTeX mathematics terminology, for any polynomial $p$ in a ring $R$, the product $\prod (X - a)$ where $a$ ranges over the roots of $p$, divides $p$.
More concisely: For any polynomial $p$ over a commutative integral domain $R$, the product of its linear factors $X - a$ for all roots $a$ of $p$ divides $p$. In Lean notation, `p` is a multiple of `prod (X : R) <- roots p`.
|
Polynomial.prime_X_sub_C
theorem Polynomial.prime_X_sub_C :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (r : R), Prime (Polynomial.X - Polynomial.C r)
The theorem `Polynomial.prime_X_sub_C` states that for all commutative rings `R` that are also integral domains, and for any element `r` in `R`, the polynomial `X - C r` (where `X` is the polynomial variable and `C r` is the constant polynomial `r`) is a prime element. Here, a prime element in a commutative monoid with zero is an element `p` that is not zero, is not a unit, and if `p` divides the product of `a` and `b`, then `p` must divide `a` or `b`.
More concisely: For any commutative domain `R`, the polynomial `X - C r` in `R[X]` is a prime element.
|
Polynomial.aeval_modByMonic_eq_self_of_root
theorem Polynomial.aeval_modByMonic_eq_self_of_root :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {p q : Polynomial R},
q.Monic →
∀ {x : S}, (Polynomial.aeval x) q = 0 → (Polynomial.aeval x) (p.modByMonic q) = (Polynomial.aeval x) p
The theorem `Polynomial.aeval_modByMonic_eq_self_of_root` states that for any commutative ring `R`, ring `S`, and an algebra structure on `S` over `R`, given two polynomials `p` and `q` over `R`, if `q` is monic (its leading coefficient is 1), then for any valuation `x` in `S` that is a root of `q` (i.e., `q` evaluated at `x` equals 0), evaluating `p` modulo `q` at `x` is the same as directly evaluating `p` at `x`. This theorem is a reflection of the fact that if `x` is a root of a monic polynomial `q`, then `x` "behaves as if `q` is zero" when evaluating any polynomial modulo `q`.
More concisely: For any commutative rings R, ring S with an algebra structure over R, monic polynomial q over R, and root x of q in S, the evaluation of p modulo q at x equals the direct evaluation of p at x.
|
Polynomial.degree_eq_zero_of_isUnit
theorem Polynomial.degree_eq_zero_of_isUnit :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p : Polynomial R} [inst_2 : Nontrivial R],
IsUnit p → p.degree = 0
The theorem `Polynomial.degree_eq_zero_of_isUnit` states that for any semiring `R` which does not contain zero divisors and is nontrivial, if a polynomial `p` over `R` is a unit (meaning it has a multiplicative inverse), then the degree of `p` is zero. In other words, a polynomial in such a ring is a unit if and only if it is a nonzero constant polynomial.
More concisely: In a semiring without zero divisors and containing only the multiplicative identity and units, every unit polynomial has degree zero.
|
Polynomial.aroots_C
theorem Polynomial.aroots_C :
∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
(a : T), (Polynomial.C a).aroots S = 0
This theorem states that for any commutative rings `S` and `T` with `S` being an integral domain and an algebra over `T`, and for any element `a` from `T`, the multiset of roots of the constant polynomial `a` (considered as a polynomial over `S`) is empty. In other words, a constant polynomial doesn't have any roots.
More concisely: For any commutative rings S and T with S an integral domain and S an algebra over T, and for any element a in T, the constant polynomial a over S has no roots.
|
Polynomial.aroots_C_mul
theorem Polynomial.aroots_C_mul :
∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
[inst_4 : NoZeroSMulDivisors T S] {a : T} (p : Polynomial T),
a ≠ 0 → (Polynomial.C a * p).aroots S = p.aroots S
The theorem `Polynomial.aroots_C_mul` states that for any commutative rings `S` and `T`, where `S` is also a domain and an algebra over `T`, and there are no zero `S`-multiples of non-zero `T` elements, given a non-zero element `a` in `T` and a polynomial `p` with coefficients in `T`, the multiset of roots of the polynomial obtained by multiplying `p` with the constant polynomial associated with `a`, when observed as a polynomial over `S`, is the same as the multiset of roots of the original polynomial `p` over `S`. In mathematical terms, if $a$ is a non-zero constant and $p(x)$ is a polynomial, then the roots of $a \cdot p(x)$ are the same as the roots of $p(x)$.
More concisely: For any commutative rings S and T with no zero-divisors in T, and where S is a domain and an algebra over T, the roots of the polynomial p(x) over S are equal to the roots of the constant multiplied by p(x) polynomial over S, for any non-zero constant a in T.
|
Polynomial.roots_zero
theorem Polynomial.roots_zero : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.roots 0 = 0 := by
sorry
The theorem `Polynomial.roots_zero` states that for any type `R` that is a commutative ring and an integral domain, the roots of the zero polynomial are an empty multiset. This is consistent with the mathematical convention, as the zero polynomial does not have any roots in an integral domain.
More concisely: In an integral domain, the zero polynomial has no roots.
|
Polynomial.card_roots
theorem Polynomial.card_roots :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
p ≠ 0 → ↑(Multiset.card p.roots) ≤ p.degree
The theorem `Polynomial.card_roots` states that for any non-zero polynomial `p` over a commutative ring `R` that is also an integral domain, the cardinality of the multiset of roots of `p` (which includes each root with its multiplicity) is less than or equal to the degree of `p`. Here, the cardinality of a multiset is defined as the sum of the multiplicities of all its elements, and the degree of a polynomial is defined as the largest exponent of `X` in the polynomial, with the degree of the zero polynomial being bottom (`⊥`).
More concisely: The number of roots (counting multiplicities) of a non-zero polynomial over a commutative integral domain is less than or equal to its degree.
|
Polynomial.roots_X
theorem Polynomial.roots_X : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.X.roots = {0} := by
sorry
This theorem states that for all types `R` that have a commutative ring structure and are integral domains, the roots of the polynomial `X` (which represents the polynomial variable or indeterminate) are given by the singleton set containing only the number zero. In other words, the only root (solution) of the polynomial `X` in any integral domain is zero.
More concisely: In an integral domain with a commutative ring structure, the polynomial `X` has only the number zero as a root.
|
Polynomial.mem_roots
theorem Polynomial.mem_roots :
∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
p ≠ 0 → (a ∈ p.roots ↔ p.IsRoot a)
This theorem states that for any type `R` and any element `a` of `R`, given that `R` is a commutative ring and a domain, and for any polynomial `p` of coefficients from `R`, if `p` is not the zero polynomial, then `a` is a root of `p` (i.e., when `p` is evaluated at `a`, the result is zero) if and only if `a` belongs to the multiset of roots of `p`. In other words, this theorem provides the equivalence between the property of `a` being a root of `p` and the property of `a` being a member of the set of roots of `p`.
More concisely: For any commutative ring and domain R, element a in R, and non-zero polynomial p over R, a is a root of p if and only if a belongs to the set of roots of p.
|
Polynomial.le_rootMultiplicity_iff
theorem Polynomial.le_rootMultiplicity_iff :
∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
p ≠ 0 → ∀ {a : R} {n : ℕ}, n ≤ Polynomial.rootMultiplicity a p ↔ (Polynomial.X - Polynomial.C a) ^ n ∣ p
This theorem states that for any commutative ring `R`, a nonzero polynomial `p` of `R`, an element `a` of `R`, and a natural number `n`, the multiplicity of `a` as a root of `p` is greater than or equal to `n` if and only if the polynomial `(X - a) ^ n` divides `p`. Here, `X` represents the polynomial variable and `C a` represents the constant polynomial `a`. The multiplicity of `a` as a root of `p` is defined as the largest power of `(X - a)` that divides `p`.
More concisely: For any commutative ring R, a nonzero polynomial p of R, an element a of R, and a natural number n, the element a is a root of multiplicity greater than or equal to n of polynomial p if and only if (X - a) ^ n divides p.
|
Polynomial.count_roots
theorem Polynomial.count_roots :
∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R] (p : Polynomial R),
Multiset.count a p.roots = Polynomial.rootMultiplicity a p
This theorem states that for any type `R`, any element `a` of `R`, and any polynomial `p` of type `R`, given that `R` is a commutative ring, `R` is a domain, and `R` has decidable equality, the count of `a` in the roots of `p` is equal to the root multiplicity of `a` in `p`. In simpler terms, the number of times a value `a` appears as a root of a polynomial `p` is exactly the same as the largest power of `(X - a)` that divides `p`.
More concisely: Given a commutative domain `R` with decidable equality, for any polynomial `p` in `R[X]`, the number of times an element `a` is a root of `p` is equal to the multiplicity of `(X - a)` as a factor of `p`.
|
Polynomial.roots_C_mul
theorem Polynomial.roots_C_mul :
∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R),
a ≠ 0 → (Polynomial.C a * p).roots = p.roots
This theorem states that for any type `R`, given a commutative ring structure and a domain structure on `R`, for any non-zero element `a` of `R` and any polynomial `p` over `R`, the roots of the polynomial obtained by multiplying `p` by the constant polynomial `a` are the same as the roots of `p`. In other words, scaling a polynomial by a non-zero constant does not change its roots.
More concisely: For any commutative ring `R`, non-zero element `a` in `R`, and polynomial `p` over `R`, the roots of the polynomial `a * p` are equal to the roots of `p`.
|
Polynomial.mem_nthRootsFinset
theorem Polynomial.mem_nthRootsFinset :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ},
0 < n → ∀ {x : R}, x ∈ Polynomial.nthRootsFinset n R ↔ x ^ n = 1
This theorem states that, for any commutative ring `R` that is also an integral domain, and for any positive natural number `n`, a given element `x` of `R` is in the finset of `n`-th roots of unity (that is, the finset of solutions to the equation `x^n = 1` in the ring `R`) if and only if `x` raised to the power of `n` equals `1`.
More concisely: For a commutative ring R that is an integral domain, an element x of R is a n-th root of unity if and only if x^n = 1.
|
Polynomial.rootSet_def
theorem Polynomial.rootSet_def :
∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra T S] [inst_4 : DecidableEq S], p.rootSet S = ↑(p.aroots S).toFinset
The theorem `Polynomial.rootSet_def` states that, for any type `T` with a commutative ring structure, a polynomial `p` with coefficients in `T`, a type `S` with a commutative ring structure and domain property, and an algebraic structure connecting `T` and `S`, along with decidable equality on `S`, the set of distinct roots of `p` in `S` is equal to the set created by removing duplicates from the multiset of roots of `p` regarded as a polynomial over `S`. In mathematical terms, this theorem asserts that the set of roots of a polynomial in an associated algebraic structure is precisely the unique roots of the polynomial considered over that structure.
More concisely: The set of distinct roots of a polynomial over a commutative ring with decidable equality is equal to the set obtained by removing duplicates from the multiset of roots regarded as a polynomial over an algebraically connected commutative ring.
|
Polynomial.degree_le_mul_left
theorem Polynomial.degree_le_mul_left :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {q : Polynomial R} (p : Polynomial R),
q ≠ 0 → p.degree ≤ (p * q).degree
The theorem `Polynomial.degree_le_mul_left` states that for any non-zero polynomial `q`, from a semiring `R` that does not allow zero divisors, the degree of any polynomial `p` is less than or equal to the degree of the product of `p` and `q`. This means that multiplying a polynomial by a non-zero polynomial cannot decrease the degree, it can only increase or keep it the same.
More concisely: For any non-zero polynomial $p$ in a semiring $R$ without zero divisors, the degree of $p$ is less than or equal to the degree of $p \cdot q$.
|
Polynomial.natDegree_le_of_dvd
theorem Polynomial.natDegree_le_of_dvd :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p q : Polynomial R},
p ∣ q → q ≠ 0 → p.natDegree ≤ q.natDegree
The theorem `Polynomial.natDegree_le_of_dvd` states that for all types `R` that form a semiring and have no zero divisors, and for all polynomials `p` and `q` defined over `R`, if `p` divides `q` and `q` is not zero, then the natural degree of `p` (obtained by the function `Polynomial.natDegree`) is less than or equal to the natural degree of `q`. In other words, the degree of a divisor polynomial is always less than or equal to the degree of the dividend polynomial, given that the dividend is not zero.
More concisely: For all semirings R without zero divisors and polynomials p, q over R with p dividing non-zero q, the natural degree of p is less than or equal to the natural degree of q.
|
Polynomial.mem_rootSet
theorem Polynomial.mem_rootSet :
∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra T S] [inst_4 : NoZeroSMulDivisors T S] {a : S},
a ∈ p.rootSet S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0
The theorem `Polynomial.mem_rootSet` states that for all types `T` and `S`, where `T` is a commutative ring and `S` is a commutative ring that is also a domain, and where `S` is an `T`-algebra which has no zero scalar multiplication and division, a value `a` of type `S` is in the set of distinct roots of a polynomial `p` of type `T` if and only if the polynomial `p` is not the zero polynomial and the unique `T`-algebra homomorphism from `T[X]` to `S` sending `X` to `a` applied to `p` equals zero. Stated more simply, `a` is a root of `p` if and only if `p` is not the zero polynomial and when `p` is evaluated at `a`, the result is zero.
More concisely: A value `a` in a commutative domain `S` that is an `T`-algebra of a commutative ring `T` with no zero scalar multiplication and division, is a root of polynomial `p` in `T[X]` if and only if `p` is not the zero polynomial and `p(a) = 0` in `S`.
|
Multiset.prod_X_sub_C_dvd_iff_le_roots
theorem Multiset.prod_X_sub_C_dvd_iff_le_roots :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
p ≠ 0 → ∀ (s : Multiset R), (Multiset.map (fun a => Polynomial.X - Polynomial.C a) s).prod ∣ p ↔ s ≤ p.roots
This theorem states that for any commutative ring `R` and any polynomial `p` in `R` that is not the zero polynomial, there is a Galois connection between a multiset `s` of elements from `R` and the roots of the polynomial `p`. Specifically, the product of the polynomials `X - C a` (where `a` ranges over elements in the multiset `s`) divides the polynomial `p` if and only if the multiset `s` is a subset of the roots of `p`. Here, `X` is the polynomial variable, `C a` is the constant polynomial `a`, and `p.roots` is the set of roots of the polynomial `p`.
More concisely: For any commutative ring R and polynomial p(X) ≠ 0 in R, there exists a Galois connection between the multiset of roots of p and the multiset of elements in R such that the product of X - a (over a in the multiset of roots) divides p if and only if the multiset contains exactly the elements that are roots of p.
|
Polynomial.nthRoots_zero
theorem Polynomial.nthRoots_zero :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (r : R), Polynomial.nthRoots 0 r = 0
The theorem `Polynomial.nthRoots_zero` states that for any ring `R` which is a commutative ring and an integral domain, and for any element `r` of `R`, the set of zeroth roots of `r` is zero. In other words, there are no solutions to the equation `x^0 = r` in the ring `R`.
More concisely: In a commutative ring and integral domain, there are no zeroth roots other than the additive identity for any element.
|
Polynomial.leadingCoeff_divByMonic_of_monic
theorem Polynomial.leadingCoeff_divByMonic_of_monic :
∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R},
q.Monic → q.degree ≤ p.degree → (p.divByMonic q).leadingCoeff = p.leadingCoeff
This theorem states that if you divide a polynomial `p` by a monic polynomial `q` (in a commutative ring `R`), the leading coefficient of the result is the same as the leading coefficient of the original polynomial `p`. This holds true under two conditions: the polynomial `q` is monic (i.e., its leading coefficient is 1), and the degree of `q` is less than or equal to the degree of `p`.
More concisely: If `p` is a polynomial and `q` is a monic divisor of `p` of degree less than or equal to that of `p`, then the leading coefficients of `p` and `p / q` are equal.
|
Polynomial.rootMultiplicity_add
theorem Polynomial.rootMultiplicity_add :
∀ {R : Type u} [inst : CommRing R] {p q : Polynomial R} (a : R),
p + q ≠ 0 →
min (Polynomial.rootMultiplicity a p) (Polynomial.rootMultiplicity a q) ≤
Polynomial.rootMultiplicity a (p + q)
This theorem states that the multiplicity of a root `a` in the polynomial `p + q` is at least the minimum of the multiplicities of `a` in `p` and `q`, provided that `p + q` is not equal to zero. Here, the root multiplicity of a root `a` in a polynomial is the largest power of `(X - a)` that divides the polynomial. This is in the context of `R` being a commutative ring.
More concisely: If `p(X)` and `q(X)` are polynomials over a commutative ring `R`, and `a` is a root of `p(X) + q(X)` with multiplicity `m`, then `m` is at least the minimum of the multiplicities of `a` in `p(X)` and `q(X)` (assuming `p(X) + q(X) \neq 0`).
|
Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq
theorem Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
p.Monic →
Multiset.card p.roots = p.natDegree →
(Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod = p
The theorem `Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq` states that for any monic polynomial `p` over a commutative ring `R` (with `R` also being an integral domain), if the cardinality (or the number of elements, counting multiplicities) of the roots of `p` is equal to its degree, then `p` can be written as the product of `(X - a)`, for each root `a` in `p.roots`. This means that `p` can be factored into linear terms, each corresponding to a root of `p`. Note that `Polynomial.X` represents the polynomial variable, `Polynomial.C a` represents the constant polynomial `a`, and `Multiset.map` is used to apply the function `(fun a => Polynomial.X - Polynomial.C a)` to each root `a` in `p.roots` to construct the aforementioned product.
More concisely: If a monic polynomial `p` of degree `n` over a commutative integral domain `R` has exactly `n` roots, then `p` can be expressed as the product of `n` linear terms, `(X - a)` for each root `a` of `p`.
|
Polynomial.Monic.irreducible_of_irreducible_map
theorem Polynomial.Monic.irreducible_of_irreducible_map :
∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : IsDomain S]
(φ : R →+* S) (f : Polynomial R), f.Monic → Irreducible (Polynomial.map φ f) → Irreducible f
This theorem states that for any two integral domains `R` and `S`, and a ring homomorphism `φ` from `R` to `S`, if a polynomial `f` over `R` is monic (the leading coefficient is one) and after applying the map `φ` to `f`, the new polynomial becomes irreducible in `S`, then the original polynomial `f` is irreducible in `R`.
A notable application of this theorem is that a polynomial over integers (`ℤ`) is irreducible if it is monic and remains irreducible when reduced modulo a prime number `p` ( operating in the ring of integers modulo `p`, `ℤ/pℤ`).
More concisely: If `φ` is a ring homomorphism from integral domains `R` to `S`, `f` is a monic polynomial over `R`, and the image of `f` under `φ` is irreducible in `S`, then `f` is irreducible in `R`.
|
Polynomial.aroots_def
theorem Polynomial.aroots_def :
∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra T S], p.aroots S = (Polynomial.map (algebraMap T S) p).roots
The theorem `Polynomial.aroots_def` states that for any given polynomial `p` with coefficients in a commutative ring `T`, and any `T`-algebra `S`, the multiset of roots of `p` when regarded as a polynomial over `S` (as denoted by `Polynomial.aroots p S`) is equal to the multiset of roots of the polynomial obtained by mapping `p` via the algebraic structure from `T` to `S` (as denoted by `Polynomial.roots (Polynomial.map (algebraMap T S) p)`). In other words, mapping a polynomial to an algebra and then finding its roots is the same as finding the roots of the original polynomial in the context of that algebra.
More concisely: For any polynomial `p` over a commutative ring `T` and `T`-algebra `S`, the multiset of roots of `p` over `S` equals the multiset of roots of the polynomial obtained by mapping `p` to `S`. (Equivalently, `Polynomial.aroots p S` = `Polynomial.roots (Polynomial.map (algebraMap T S) p)`)
|
Polynomial.mem_rootSet'
theorem Polynomial.mem_rootSet' :
∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra T S] {a : S},
a ∈ p.rootSet S ↔ Polynomial.map (algebraMap T S) p ≠ 0 ∧ (Polynomial.aeval a) p = 0
The theorem `Polynomial.mem_rootSet'` states the following: For any commutative ring `T` and any polynomial `p` with coefficients in `T`, and for any other commutative ring `S` which is also assumed to be a domain, and an algebra over `T`, and an element `a` in `S`, `a` is a root of the polynomial `p` in `S` if and only if the image of the polynomial `p` under the ring homomorphism from `T` to `S` (given by the algebra structure) is nonzero and the polynomial `p` evaluated at `a` (using the unique algebra homomorphism from the polynomial ring over `T` to `S` that sends the variable to `a`) is zero.
This means that `a` is a root of `p` in `S` precisely when `p` doesn't map to the zero polynomial in `S` and `p` evaluated at `a` yields zero.
More concisely: A element `a` in a commutative ring `S` is a root of polynomial `p` with coefficients in a commutative ring `T` if and only if the image of `p` under the ring homomorphism from `T` to `S` is nonzero and `p(a)` equals zero in `S`.
|
Polynomial.roots_C
theorem Polynomial.roots_C :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (x : R), (Polynomial.C x).roots = 0
The theorem `Polynomial.roots_C` states that for any commutative ring `R` that is also an integral domain, and any element `x` from `R`, the roots of the constant polynomial `C x` (i.e., a polynomial that has the same value `x` at every point) are an empty set. In other words, a constant polynomial has no roots.
More concisely: In an integral domain, the constant polynomial has no roots.
|
Polynomial.roots_mul
theorem Polynomial.roots_mul :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p q : Polynomial R},
p * q ≠ 0 → (p * q).roots = p.roots + q.roots
The theorem `Polynomial.roots_mul` states that for any commutative ring `R` with unity, given that `R` is an integral domain and `p` and `q` are polynomials over `R`, if the product of `p` and `q` is not equal to zero, then the roots of the polynomial resulting from the product of `p` and `q` is equal to the sum of the roots of `p` and the roots of `q`. This means that the roots of the multiplied polynomials are the union of the roots of the original polynomials, including their multiplicities.
More concisely: If `R` is a commutative ring with unity, an integral domain, and `p` and `q` are non-zero polynomials over `R`, then the roots of `p * q` are the union of the roots of `p` and `q`, each root having multiplicity equal to its multiplicity in `p` plus its multiplicity in `q`.
|
Polynomial.bUnion_roots_finite
theorem Polynomial.bUnion_roots_finite :
∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : DecidableEq S] (m : R →+* S) (d : ℕ) {U : Set R},
U.Finite →
(⋃ f, ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U), ↑(Polynomial.map m f).roots.toFinset).Finite
This theorem states that for any semiring `R`, commutative ring `S` where `S` is a domain and has decidable equality, given a ring homomorphism `m` from `R` to `S`, a natural number `d` and a finite set `U` of elements in `R`, the set of roots of all polynomials of degree at most `d` and whose coefficients are in `U`, under the mapping of `m`, is finite. This is essentially saying that the set of roots of a finite set of bounded degree polynomials with coefficients from a finite set is finite when these polynomials are mapped across a ring homomorphism.
More concisely: For any commutative ring S a domain with decidable equality, given a ring homomorphism m from semiring R to S and a finite set U of elements in R, the set of roots of polynomials of degree at most d in R with coefficients in U, under the mapping of m, is finite.
|
Polynomial.isUnit_iff
theorem Polynomial.isUnit_iff :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p : Polynomial R},
IsUnit p ↔ ∃ r, IsUnit r ∧ Polynomial.C r = p
This theorem characterizes a unit of a polynomial ring over an integral domain `R`. It states that for any semiring `R` that has no zero divisors and any polynomial `p` over `R`, `p` is a unit if and only if there exists a `r` in `R` such that `r` is a unit and the constant polynomial of `r` is equal to `p`. It's worth noting that in the context of this theorem, a unit is defined as an element of a Monoid that has a two-sided inverse. The theorem is a specific case when `R` is an integral domain, and there is a more general version of this theorem when `R` is a commutative ring.
More concisely: A polynomial over an integral domain with no zero divisors is a unit if and only if there exists a unit in the domain whose constant polynomial is equal to the polynomial.
|
Polynomial.irreducible_X
theorem Polynomial.irreducible_X : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Irreducible Polynomial.X
This theorem states that for any type `R` which is a commutative ring and also a domain, the polynomial variable `X` is irreducible. In mathematical terms, in any integral domain `R`, the polynomial `X` (which represents a variable or indeterminate) cannot be factored into two non-unit polynomials, which is the definition of an irreducible polynomial.
More concisely: In a commutative domain `R`, the polynomial `X` is irreducible.
|