Polynomial.map_ne_zero
theorem Polynomial.map_ne_zero :
∀ {R : Type u} {S : Type v} [inst : DivisionRing R] {p : Polynomial R} [inst_1 : Semiring S] [inst_2 : Nontrivial S]
{f : R →+* S}, p ≠ 0 → Polynomial.map f p ≠ 0
The theorem `Polynomial.map_ne_zero` states that for any types `R` and `S`, given a division ring over `R`, a polynomial `p` in `R`, a semiring over `S`, and a nontrivial ring homomorphism `f` from `R` to `S`, if the polynomial `p` is not equal to zero, then the mapped polynomial (obtained by mapping `p` across the ring hom `f`) is also not equal to zero. In other words, non-zero polynomials remain non-zero under nontrivial ring homomorphisms.
More concisely: If `f` is a nontrivial ring homomorphism from a division ring `R` to a semiring `S`, and `p` is a non-zero polynomial in `R`, then the mapped polynomial `f(p)` is also a non-zero polynomial in `S`.
|
Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero
theorem Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero :
∀ {K : Type u_1} [inst : Field K] (f : Polynomial K) (a : K),
Polynomial.eval a (Polynomial.derivative f) ≠ 0 →
IsCoprime (Polynomial.X - Polynomial.C a) (f.divByMonic (Polynomial.X - Polynomial.C a))
The theorem `Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero` states that for any field `K` and any polynomial `f` over `K`, if a value `a` from `K` is such that the derivative of `f` evaluated at `a` is not zero, then the polynomial `f` divided by `(X - a)` is coprime with `(X - a)`. Note that this theorem does not assume that `f(a) = 0`, because `f / (X - a)` is equivalent to `(f - f(a)) / (X - a)`. In this context, two polynomials being coprime means that there exist two other polynomials such that the sum of their products with the original polynomials equals one.
More concisely: Given a field `K` and a polynomial `f` over `K`, if the derivative of `f` evaluated at `a` in `K` is non-zero, then `f` and `X - a` are coprime polynomials over `K`.
|
Polynomial.div_def
theorem Polynomial.div_def :
∀ {R : Type u} [inst : Field R] {p q : Polynomial R},
p / q = Polynomial.C q.leadingCoeff⁻¹ * p.divByMonic (q * Polynomial.C q.leadingCoeff⁻¹)
This theorem states that for any field `R` and any polynomials `p` and `q` over `R`, the quotient of `p` divided by `q` equals the constant polynomial of the inverse of the leading coefficient of `q` times the pseudoquotient of `p` and the product of `q` and the constant polynomial of the inverse of the leading coefficient of `q`. In other words, the theorem gives a definition of polynomial division in terms of the inverse of the leading coefficient of the divisor and pseudo-division (`/ₘ` is the notation for pseudo-division in Lean 4).
More concisely: For any field `R` and polynomials `p` and `q` over `R` with non-zero leading coefficients, `p / q = (lc(q)⁻¹ * p) /ₘ (lc(q) * q)`, where `lc` denotes the leading coefficient and `/ₘ` represents pseudo-division.
|
Polynomial.natDegree_map
theorem Polynomial.natDegree_map :
∀ {R : Type u} {S : Type v} [inst : DivisionRing R] {p : Polynomial R} [inst_1 : Semiring S] [inst_2 : Nontrivial S]
(f : R →+* S), (Polynomial.map f p).natDegree = p.natDegree
The theorem `Polynomial.natDegree_map` states that for any division ring `R`, any polynomial `p` over `R`, any semiring `S` that is nontrivial, and any ring homomorphism `f` from `R` to `S`, the natural degree of the polynomial obtained by mapping `p` across `f` is equal to the natural degree of `p`. In other words, mapping a polynomial across a ring homomorphism does not change its natural degree. This can be mathematically represented as $\text{{natDegree}}(\text{{map}}(f, p)) = \text{{natDegree}}(p)$.
More concisely: The natural degree of a polynomial mapped across a ring homomorphism remains unchanged.
|
Polynomial.isUnit_iff_degree_eq_zero
theorem Polynomial.isUnit_iff_degree_eq_zero :
∀ {R : Type u} [inst : Field R] {p : Polynomial R}, IsUnit p ↔ p.degree = 0
The theorem `Polynomial.isUnit_iff_degree_eq_zero` states that for any given field `R`, and any polynomial `p` over `R`, the polynomial `p` is a unit (i.e., it has a two-sided inverse) if and only if the degree of the polynomial `p` is zero. Here, the degree of a polynomial is defined as the highest power of `X` that appears in the polynomial, or `⊥` (bottom) in the case of the zero polynomial. This is a property of fields, which are algebraic structures with operations analogous to those of the field of real numbers.
More concisely: A polynomial over a field is a unit if and only if its degree is zero.
|
Polynomial.coe_normUnit
theorem Polynomial.coe_normUnit :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizationMonoid R] {p : Polynomial R},
↑(normUnit p) = Polynomial.C ↑(normUnit p.leadingCoeff)
This theorem states that for any commutative ring `R` that is also an integral domain and a normalization monoid, and for any polynomial `p` with coefficients in `R`, the unit normalization of `p` (denoted by `normUnit p`) is equal to the constant polynomial with the unit normalization of the leading coefficient of `p` as its constant term. In other words, the unit normalization of a polynomial equals a constant polynomial whose constant term is the unit normalization of the leading coefficient of the original polynomial.
More concisely: For any commutative ring R that is an integral domain and a normalization monoid, the unit normalization of a polynomial p over R equals the constant polynomial with the unit normalization of p's leading coefficient as its constant term.
|
Polynomial.map_eq_zero
theorem Polynomial.map_eq_zero :
∀ {R : Type u} {S : Type v} [inst : DivisionRing R] {p : Polynomial R} [inst_1 : Semiring S] [inst_2 : Nontrivial S]
(f : R →+* S), Polynomial.map f p = 0 ↔ p = 0
The theorem `Polynomial.map_eq_zero` states that for any type `R` that is a Division Ring, a type `S` that is a Semiring and is nontrivial, a polynomial `p` of type `R`, and a ring homomorphism `f` from `R` to `S`, the mapping of the polynomial `p` across the ring homomorphism `f` results in the zero polynomial if and only if the original polynomial `p` is the zero polynomial. In other words, a polynomial maps to the zero polynomial under a ring homomorphism if and only if it is the zero polynomial.
More concisely: For any Division Ring R, Semiring S (nontrivial), polynomial p in R, and ring homomorphism f from R to S, p maps to the zero polynomial in S if and only if p is the zero polynomial in R.
|
Polynomial.degree_pos_of_irreducible
theorem Polynomial.degree_pos_of_irreducible :
∀ {R : Type u} [inst : Field R] {p : Polynomial R}, Irreducible p → 0 < p.degree
This theorem states that for any given irreducible polynomial `p` over a field `R`, the degree of `p` is positive. In other words, if `p` is a polynomial that cannot be factored into a product of two non-unit polynomials in the field `R`, then the highest power of `X` that appears in `p` is greater than zero.
More concisely: Every irreducible polynomial over a field has positive degree.
|
Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors
theorem Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors :
∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
p ≠ 0 →
(∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) →
↑n.factorial ∈ nonZeroDivisors R → n < Polynomial.rootMultiplicity t p
This theorem states that for any commutative ring `R`, given a non-zero polynomial `p` of type `R`, a scalar `t` of type `R`, and a natural number `n`, if `t` is a root of the `m`-th derivative of `p` for all `m` less than or equal to `n`, and the factorial of `n` is a member of the non-zero divisors of `R`, then `n` is strictly less than the root multiplicity of `t` in `p`. In other words, if a number is a root of a polynomial and its derivatives up to a certain order, then the multiplicity of that root in the polynomial is greater than that order, provided that the factorial of the order is a non-zero divisor.
More concisely: If `p` is a non-zero polynomial in a commutative ring `R`, `t` is a root of the derivatives of `p` up to order `n` (`n` being a natural number), and the factorial `n!` is a non-zero divisor in `R`, then the multiplicity of `t` as a root of `p` is strictly greater than `n`.
|
Polynomial.leadingCoeff_map
theorem Polynomial.leadingCoeff_map :
∀ {R : Type u} {S : Type v} [inst : DivisionRing R] {p : Polynomial R} [inst_1 : Semiring S] [inst_2 : Nontrivial S]
(f : R →+* S), (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
The theorem `Polynomial.leadingCoeff_map` states that for any polynomial `p` over a division ring `R` and any ring homomorphism `f` from `R` to a semiring `S` (which is nontrivial), the leading coefficient of the polynomial obtained by mapping `p` across `f` is equal to the image of the leading coefficient of `p` under `f`. In other words, applying the ring homomorphism `f` to `p` does not change the leading coefficient of `p`, but merely transforms it via `f`.
More concisely: For any polynomial $p$ over a division ring $R$ and ring homomorphism $f$ from $R$ to a semiring $S$, the leading coefficient of $f(p)$ is $f(\text{lc}(p))$, where $\text{lc}(p)$ denotes the leading coefficient of $p$.
|
Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity
theorem Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity :
∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
n < Polynomial.rootMultiplicity t p → ((⇑Polynomial.derivative)^[n] p).IsRoot t
The theorem `Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity` states that for any commutative ring `R`, polynomial `p` of `R`, variable `t` of `R`, and natural number `n`, if `n` is less than the root multiplicity of `t` in `p` then `t` is a root of the `n`-th derivative of `p`. In other words, if a number `t` is a root of a polynomial `p` with multiplicity greater than `n`, then `t` is also a root of the `n`-th derivative of `p`.
More concisely: If the root multiplicity of `t` in polynomial `p` is greater than the degree of the derivative `p.derivative(n)`, then `t` is a root of `p.derivative(n)`.
|
Polynomial.degree_map
theorem Polynomial.degree_map :
∀ {R : Type u} {S : Type v} [inst : DivisionRing R] [inst_1 : Semiring S] [inst_2 : Nontrivial S] (p : Polynomial R)
(f : R →+* S), (Polynomial.map f p).degree = p.degree
This theorem, `Polynomial.degree_map`, states that for any division ring `R`, semiring `S` with nontrivial element, any polynomial `p` of type `R`, and any ring homomorphism `f` from `R` to `S`, the degree of the polynomial obtained by mapping `p` with `f` is equal to the degree of the original polynomial `p`. In other words, the process of mapping a polynomial across a ring homomorphism does not change its degree. This suggests that the degree of a polynomial is invariant under the homomorphism.
More concisely: For any division ring R, semiring S with nontrivial element, polynomial p over R, and ring homomorphism f from R to S, the degree of the polynomial f(p) is equal to the degree of p.
|