Polynomial.natDegree_comp
theorem Polynomial.natDegree_comp :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p q : Polynomial R},
(p.comp q).natDegree = p.natDegree * q.natDegree
The theorem `Polynomial.natDegree_comp` states that for any semiring `R` that has no zero divisors, and for any two polynomials `p` and `q` over `R`, the natural degree of the composition of `p` and `q` is equal to the product of the natural degree of `p` and the natural degree of `q`. The natural degree of a polynomial is the degree forced to be a natural number, with the degree of the zero polynomial defined as zero. The composition of two polynomials is a new polynomial achieved by substituting `q` into `p`.
More concisely: For polynomials $p$ and $q$ over a semiring $R$ without zero divisors, the natural degree of their composition $p \circ q$ is equal to the product of the natural degrees of $p$ and $q$.
|
Polynomial.irreducible_mul_leadingCoeff_inv
theorem Polynomial.irreducible_mul_leadingCoeff_inv :
∀ {K : Type u_1} [inst : DivisionRing K] {p : Polynomial K},
Irreducible (p * Polynomial.C p.leadingCoeff⁻¹) ↔ Irreducible p
This theorem states that for any division ring `K` and any polynomial `p` over `K`, the polynomial `p` is irreducible if and only if the product of `p` and the inverse of the constant polynomial of the leading coefficient of `p` is also irreducible. Here, irreducibility refers to the property of a polynomial that it cannot be factored into a product of two non-constant polynomials. In mathematical notation, this would read as `p` is irreducible if and only if `p * C(leadingCoeff(p))⁻¹` is irreducible, where `C(a)` represents a constant polynomial `a` and `leadingCoeff(p)` is the coefficient of the highest power of `X` in `p`.
More concisely: A polynomial `p` over a division ring `K` is irreducible if and only if the constant polynomial `C(leadingCoeff(p))⁻¹ * p` is irreducible.
|
Polynomial.natDegree_pos_of_nextCoeff_ne_zero
theorem Polynomial.natDegree_pos_of_nextCoeff_ne_zero :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.nextCoeff ≠ 0 → 0 < p.natDegree
This theorem states that for any semiring `R` and any polynomial `p` of type `R`, if the second-highest coefficient of the polynomial (referred to as `Polynomial.nextCoeff p`) is not equal to zero, then the natural degree of the polynomial (referred to as `Polynomial.natDegree p`) must be greater than zero. In other words, if a polynomial has a non-zero second-highest coefficient, then its degree must be positive.
More concisely: If `p` is a polynomial over a semiring `R` with non-zero second-highest coefficient, then the degree of `p` is positive.
|
Polynomial.leadingCoeff_comp
theorem Polynomial.leadingCoeff_comp :
∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p q : Polynomial R},
q.natDegree ≠ 0 → (p.comp q).leadingCoeff = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
This theorem states that for any semiring `R` that does not permit zero divisors, and for any polynomials `p` and `q` over `R`, if the natural degree of polynomial `q` is not zero, then the leading coefficient of the composition of `p` and `q` is equal to the product of the leading coefficient of `p` and the leading coefficient of `q` raised to the power of the natural degree of `p`. In other words, if we compose `p` and `q`, the coefficient of the highest power term in the resulting polynomial is determined by the leading coefficients and the degree of the original polynomials. This theorem essentially gives a rule for the leading coefficient of the polynomial resulting from the composition of two other polynomials.
More concisely: For any semirings without zero divisors, the leading coefficient of the product of polynomials `p` and `q` is equal to the product of their leading coefficients raised to the power of the degrees of `p` and `q`, respectively.
|
Polynomial.natDegree_mul_leadingCoeff_inv
theorem Polynomial.natDegree_mul_leadingCoeff_inv :
∀ {K : Type u_1} [inst : DivisionRing K] (p : Polynomial K) {q : Polynomial K},
q ≠ 0 → (p * Polynomial.C q.leadingCoeff⁻¹).natDegree = p.natDegree
The theorem `Polynomial.natDegree_mul_leadingCoeff_inv` states that for any division ring `K` (a ring in which every non-zero element has a multiplicative inverse), given any polynomials `p` and `q` in `K` where `q` is not equal to zero, the natural degree of the polynomial resulting from multiplying `p` by the multiplicative inverse of the leading coefficient of `q` (denoted by `Polynomial.leadingCoeff q`⁻¹) is equal to the natural degree of `p`. In other words, multiplying a polynomial by the inverse of the leading coefficient of another non-zero polynomial does not change the natural degree of the original polynomial.
More concisely: For any division ring K and polynomials p and q in K with q != 0, the natural degree of p * leadingCoeff(q)⁻¹ is equal to the natural degree of p.
|
Polynomial.natDegree_C_mul_eq_of_mul_ne_zero
theorem Polynomial.natDegree_C_mul_eq_of_mul_ne_zero :
∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
a * p.leadingCoeff ≠ 0 → (Polynomial.C a * p).natDegree = p.natDegree
The theorem `Polynomial.natDegree_C_mul_eq_of_mul_ne_zero` states that for any semiring `R`, any element `a` of `R`, and any polynomial `p` over `R`, if the product of `a` and the leading coefficient of `p` is not zero, then the natural degree of the polynomial obtained by multiplying `p` with the constant polynomial `a` (`Polynomial.C a * p`) is equal to the natural degree of `p` itself. It's implicitly assumed that polynomial `p` is non-zero because it's stated that `p.leadingCoeff ≠ 0`.
More concisely: If `a` is an element of a semiring `R`, and `p` is a non-zero polynomial over `R` with leading coefficient `lc`, then the natural degree of `lc * Polynomial.C a` is equal to the natural degree of `p`.
|
Polynomial.natDegree_C_mul_le
theorem Polynomial.natDegree_C_mul_le :
∀ {R : Type u} [inst : Semiring R] (a : R) (f : Polynomial R), (Polynomial.C a * f).natDegree ≤ f.natDegree := by
sorry
This theorem states that for any semiring `R`, any element `a` from `R`, and any polynomial `f` over `R`, the natural degree of the polynomial obtained by multiplying the constant polynomial `a` and `f` is less than or equal to the natural degree of `f`. In mathematical terms, if we denote the natural degree of a polynomial `p` as `deg(p)`, then for any constant `a` and any polynomial `f`, we have `deg(a*f) ≤ deg(f)`.
More concisely: For any constant `a` and polynomial `f` in a semiring, the degree of their product `a * f` is less than or equal to the degree of `f`.
|
Polynomial.natDegree_mul_C_eq_of_mul_ne_zero
theorem Polynomial.natDegree_mul_C_eq_of_mul_ne_zero :
∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R},
p.leadingCoeff * a ≠ 0 → (p * Polynomial.C a).natDegree = p.natDegree
This theorem states that for any type `R`, scalar `a`, and polynomial `p` within a semiring, if the product of the leading coefficient of `p` and `a` is non-zero, then the degree of the polynomial resulting from the multiplication of `p` and the constant polynomial `a` is equal to the degree of `p`. This implies that multiplying a polynomial by a non-zero constant does not change the degree of the polynomial.
More concisely: For any semiring `R`, polynomial `p` of degree `n` over `R`, and scalar `a` in `R` with non-zero leading coefficient of `p` multiplied by `a`, the degree of the resulting polynomial is equal to `n`.
|
Polynomial.monic_mul_leadingCoeff_inv
theorem Polynomial.monic_mul_leadingCoeff_inv :
∀ {K : Type u_1} [inst : DivisionRing K] {p : Polynomial K}, p ≠ 0 → (p * Polynomial.C p.leadingCoeff⁻¹).Monic := by
sorry
The theorem `Polynomial.monic_mul_leadingCoeff_inv` states that for every nonzero polynomial `p` over a division ring `K`, the polynomial obtained by multiplying `p` by the inverse of its leading coefficient (which is a constant polynomial), is monic. In other words, if you "normalize" a polynomial by its leading coefficient, the resulting polynomial has leading coefficient 1, which is the definition of being monic.
More concisely: For any nonzero polynomial $p$ over a division ring $K$, the polynomial $p \cdot (\text{lc}(p))^{-1}$ is monic, where $\text{lc}(p)$ is the leading coefficient of $p$.
|
Polynomial.degree_mul_leadingCoeff_inv
theorem Polynomial.degree_mul_leadingCoeff_inv :
∀ {K : Type u_1} [inst : DivisionRing K] (p : Polynomial K) {q : Polynomial K},
q ≠ 0 → (p * Polynomial.C q.leadingCoeff⁻¹).degree = p.degree
The theorem `Polynomial.degree_mul_leadingCoeff_inv` states that for any division ring `K`, and any polynomials `p` and `q` over `K` such that `q` is not the zero polynomial, the degree of the polynomial obtained by multiplying `p` by the inverse of the leading coefficient of `q` (expressed as a constant polynomial) is equal to the degree of `p`. In other words, multiplying a polynomial by the inverse of the leading coefficient of another polynomial does not change the degree of the original polynomial.
More concisely: For any division ring K and polynomials p and q over K with q not the zero polynomial, the degree of p \* (lc q)\^(-1) is equal to the degree of p. Here, lc denotes the leading coefficient.
|