Polynomial.natDegree_ne_zero_induction_on
theorem Polynomial.natDegree_ne_zero_induction_on :
∀ {R : Type u} [inst : Semiring R] {M : Polynomial R → Prop} {f : Polynomial R},
f.natDegree ≠ 0 →
(∀ {a : R} {p : Polynomial R}, M p → M (Polynomial.C a + p)) →
(∀ {p q : Polynomial R}, M p → M q → M (p + q)) →
(∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((Polynomial.monomial n) a)) → M f
This theorem states that if a property `M` holds for all polynomials with non-zero natural degree and coefficients in a semiring `R`, then it must also hold for the polynomial `f` if `f` has a non-zero natural degree. The property `M` must hold under the following conditions:
* For any polynomial `p` and any element `a` in the semiring `R`, if `M` holds for `p`, then `M` also holds for `p + a` (where `a` is treated as a constant polynomial).
* For any two polynomials `p` and `q`, if `M` holds for `p` and `q` separately, then `M` also holds for the sum `p + q`.
* For any monomial with a non-zero coefficient `a` and a non-zero exponent `n`, `M` holds for `a * X^n`.
Note that there is no explicit condition regarding multiplication in this theorem, but multiplication is implicitly involved in the condition about monomials.
More concisely: If `M` is a property that preserves addition of polynomials with non-zero natural degree and multiplication by monomials with non-zero coefficients and exponents, then `M` holds for any polynomial of non-zero natural degree in a semiring `R`.
|
Polynomial.divX_mul_X_add
theorem Polynomial.divX_mul_X_add :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.divX * Polynomial.X + Polynomial.C (p.coeff 0) = p := by
sorry
The theorem `Polynomial.divX_mul_X_add` asserts that for any polynomial `p` over a semiring `R`, the polynomial resulting from multiplying the polynomial `divX(p)` (which gives a polynomial `q` such that `q * X + C(p.coeff 0) = p`) with the polynomial variable `X` and then adding the constant polynomial of the coefficient of `X^0` in `p` (`Polynomial.C (Polynomial.coeff p 0)`), is equal to the original polynomial `p`. In mathematical terms, if `p` is a polynomial, `divX(p)` is a polynomial `q` such that `q * X + C(p.coeff 0) = p`, then for all polynomials `p` over a semiring `R`, we have `q * X + C(p.coeff 0) = p`.
More concisely: For any polynomial `p` over a semiring `R`, the polynomial `q * X + C(p.coeff 0)` equals `p`, where `q` is the polynomial obtained from dividing `p` by `X` using the division-by-x construction and `C` denotes the constant polynomial.
|
Polynomial.degree_pos_induction_on
theorem Polynomial.degree_pos_induction_on :
∀ {R : Type u} [inst : Semiring R] {P : Polynomial R → Prop} (p : Polynomial R),
0 < p.degree →
(∀ {a : R}, a ≠ 0 → P (Polynomial.C a * Polynomial.X)) →
(∀ {p : Polynomial R}, 0 < p.degree → P p → P (p * Polynomial.X)) →
(∀ {p : Polynomial R} {a : R}, 0 < p.degree → P p → P (p + Polynomial.C a)) → P p
This theorem states that, given a semiring `R` and a property `P` applicable to polynomials over `R`, if `P` holds for the polynomial `a * X` where `a` is a non-zero element of `R`, for the polynomial `p * X` where `p` is a polynomial of positive degree, and for the polynomial `p + a` where `p` is a polynomial of positive degree and `a` is an element of `R`, then `P` holds for all polynomials of positive degree over `R`. This is essentially a form of structural induction for polynomials of positive degree, based on their construction from the constant polynomial and the polynomial variable `X`.
More concisely: If a property `P` holds for the constant polynomial, the polynomial variable `X`, and the sum and product of polynomials of positive degree over a semiring `R` with a non-zero element `a`, then `P` holds for all polynomials of positive degree over `R`.
|
Polynomial.coeff_divX
theorem Polynomial.coeff_divX :
∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.divX.coeff n = p.coeff (n + 1)
This theorem, `Polynomial.coeff_divX`, states that for any semiring `R`, any natural number `n` and any polynomial `p` with coefficients in `R`, the coefficient of `X^n` in the polynomial obtained by dividing `p` by `X` (using the `Polynomial.divX` operation) is equal to the coefficient of `X^{n+1}` in the original polynomial `p`. In other words, dividing a polynomial by `X` shifts the coefficients to the lower degrees.
More concisely: For any semiring R, natural number n, and polynomial p over R in X, the coefficient of X^(n+1) in the polynomial p obtained by dividing p by X is equal to the coefficient of X^n in the original polynomial p.
|