Polynomial.support_scaleRoots_le
theorem Polynomial.support_scaleRoots_le :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R), (p.scaleRoots s).support ≤ p.support
This theorem states that for any polynomial `p` and scalar `s`, from a semiring `R`, the support (the set of all exponents `n` in the polynomial where the coefficient of `X^n` is non-zero) of the polynomial obtained by scaling the roots of `p` by `s` is a subset of or equal to the support of the original polynomial `p`. In other words, the support of the scaled polynomial is less than or equal to the support of the original polynomial. This result ensures that scaling the roots of a polynomial does not introduce any new non-zero coefficients at exponents that were not present in the original polynomial.
More concisely: The support of a polynomial obtained by scaling its roots is a subset of the support of the original polynomial in any semiring.
|
IsUnit.scaleRoots_dvd_iff
theorem IsUnit.scaleRoots_dvd_iff :
∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {r : R},
IsUnit r → (p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q)
This theorem, named `IsUnit.scaleRoots_dvd_iff`, states that for any commutative semiring `R`, given polynomials `p` and `q` in `R`, and a unit element `r` in `R`, the property that the polynomial obtained by scaling the roots of `p` by `r` divides the polynomial obtained by scaling the roots of `q` by `r` is equivalent to `p` dividing `q`. In simpler terms, scaling the roots of two polynomials by a unit does not change the divisibility relationship between the two polynomials.
More concisely: For any commutative semiring R, polynomials p and q, and a unit element r in R, the roots of p scaled by r divide the roots of q scaled by r if and only if p divides q.
|
Polynomial.coeff_scaleRoots_natDegree
theorem Polynomial.coeff_scaleRoots_natDegree :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R),
(p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
This theorem states that for any semiring `R`, polynomial `p` of type `R`, and scalar `s` of type `R`, the coefficient of the term with the highest degree in the polynomial obtained by scaling the roots of `p` by `s` (`Polynomial.scaleRoots p s`) is equal to the leading coefficient of `p` (`Polynomial.leadingCoeff p`).
In other words, the scaling of roots does not change the leading coefficient of the polynomial. In mathematical terms, if `p` is a polynomial and `s` is a scalar, then the coefficient of the highest degree term in the polynomial `p` whose roots are multiplied by `s` will be the same as the coefficient of the highest degree term in the original polynomial `p`.
More concisely: For any semiring `R`, polynomial `p` of type `R`, and scalar `s` of type `R`, the leading coefficient of the polynomial obtained by scaling the roots of `p` by `s` (`Polynomial.scaleRoots p s`) equals the leading coefficient of `p` (`Polynomial.leadingCoeff p`).
|
Polynomial.coeff_scaleRoots
theorem Polynomial.coeff_scaleRoots :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R) (i : ℕ),
(p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)
The theorem `Polynomial.coeff_scaleRoots` states that for any semiring `R`, any polynomial `p` of type `R`, any scalar `s` of type `R`, and any natural number `i`, the coefficient of the `i`-th term of the polynomial obtained by scaling the roots of `p` by `s` (`Polynomial.scaleRoots p s`) is equal to the coefficient of the `i`-th term of `p` (`Polynomial.coeff p i`) multiplied by `s` raised to the power of the difference between the degree of `p` and `i` (`s ^ (Polynomial.natDegree p - i)`). In mathematical terms, if a polynomial $p$ has degree $n$ and its roots are scaled by a scalar $s$, then the coefficient of $X^i$ in the resulting polynomial is equal to the coefficient of $X^i$ in $p$ multiplied by $s^{(n - i)}$.
More concisely: For any polynomial $p$ of degree $n$ over a semiring $R$ and scalar $s$ in $R$, the coefficient of the $i$-th term in the polynomial obtained by scaling the roots of $p$ by $s$ is equal to the coefficient of the $i$-th term in $p$ multiplied by $s^{n-i}$.
|
Polynomial.mul_scaleRoots
theorem Polynomial.mul_scaleRoots :
∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
This theorem states that, for any commutative semiring `R`, and any polynomials `p` and `q` over `R`, as well as any element `r` of `R`, scaling the roots of the product of `p` and `q` by `r` (followed by scaling by `r` raised to the power of the sum of the natural degrees of `p` and `q` minus the natural degree of their product) results in the same polynomial as scaling the roots of `p` and `q` by `r` separately and then multiplying the results.
More concisely: For any commutative semiring `R`, and polynomials `p` and `q` over `R`, the roots of `r*p*q` are the same as the roots of `r*p` and `r*q` multiplied together, where `r` is an element of `R` and degrees(p*q) = degrees(p) + degrees(q).
|
Polynomial.natDegree_scaleRoots
theorem Polynomial.natDegree_scaleRoots :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R), (p.scaleRoots s).natDegree = p.natDegree := by
sorry
This theorem states that for any semiring `R`, any polynomial `p` over `R`, and any scalar `s` in `R`, the natural degree of the polynomial obtained by scaling the roots of `p` by `s` is equal to the natural degree of `p`. In other words, scaling the roots of a polynomial does not change its natural degree. Here, the natural degree of a polynomial is the highest power of the variable that appears with a non-zero coefficient, and if the polynomial is zero, its natural degree is defined as zero.
More concisely: For any semiring `R`, scaling the roots of a polynomial `p` over `R` by a scalar `s` in `R` preserves the natural degree of `p`.
|
Dvd.dvd.scaleRoots
theorem Dvd.dvd.scaleRoots :
∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) {r : R} [inst_1 : NoZeroDivisors R],
p ∣ q → p.scaleRoots r ∣ q.scaleRoots r
This theorem, named `Dvd.dvd.scaleRoots`, states that for any type `R` that is a `CommSemiring` and also has no zero divisors, given two polynomials `p` and `q` and a scalar `r` of type `R`, if `p` divides `q`, then the scaled polynomial `p.scaleRoots r` also divides the scaled polynomial `q.scaleRoots r`. Here, "scaling roots" means multiplying all roots of the polynomial by `r`.
More concisely: If `R` is a commutative semiring without zero divisors, and `p` divides `q` in `R[x]`, then `p.scaleRoots r` divides `q.scaleRoots r` in `R[x]`, for any scalar `r` in `R`.
|
IsCoprime.scaleRoots
theorem IsCoprime.scaleRoots :
∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
IsUnit r → IsCoprime p q → IsCoprime (p.scaleRoots r) (q.scaleRoots r)
This theorem, named `IsCoprime.scaleRoots`, establishes that in the context of a commutative semiring `R`, for any two polynomials `p` and `q`, and an element `r` from `R` that is a unit, if `p` and `q` are coprime, then the polynomials obtained by scaling the roots of `p` and `q` by `r` are also coprime. The term "coprime" is used in the sense that there exist elements `a` and `b` such that `a * p + b * q = 1`. "Scaling the roots" of a polynomial effectively means multiplying all the roots by a certain value, in this case, the unit `r`.
More concisely: If `p` and `q` are coprime polynomials in a commutative semiring `R`, and `r` is a unit in `R`, then the polynomials obtained by scaling the roots of `p` and `q` by `r` are also coprime.
|