Polynomial.induction_with_natDegree_le
theorem Polynomial.induction_with_natDegree_le :
∀ {R : Type u_1} [inst : Semiring R] (P : Polynomial R → Prop) (N : ℕ),
P 0 →
(∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → P (Polynomial.C r * Polynomial.X ^ n)) →
(∀ (f g : Polynomial R), f.natDegree < g.natDegree → g.natDegree ≤ N → P f → P g → P (f + g)) →
∀ (f : Polynomial R), f.natDegree ≤ N → P f
The theorem `Polynomial.induction_with_natDegree_le` is an induction principle for polynomials. Given a property `P` that applies to polynomials over a semiring `R`, a natural number `N`, and assuming that `P` holds for the zero polynomial and for any polynomial that is the product of a non-zero constant `r` and the indeterminate `X` raised to a power `n` not greater than `N`, then if `P` holds for two polynomials `f` and `g` such that the degree of `f` is less than the degree of `g` and the degree of `g` is not greater than `N`, it also holds for their sum. Under these assumptions, the theorem states that the property `P` will hold for any polynomial whose degree is not greater than `N`.
More concisely: If `P` holds for the zero polynomial, constants, and polynomials `X^n` with `n` up to `N`, and `P` transively holds for polynomials `f` and `g` with degrees `<` and `<= N`, respectively, then `P` holds for all polynomials of degree `<= N`.
|
Polynomial.eraseLead_support
theorem Polynomial.eraseLead_support :
∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.eraseLead.support = f.support.erase f.natDegree := by
sorry
This theorem states that for any polynomial `f` over a semiring `R`, the support set (the set of all exponents `n` such that `X^n` has a non-zero coefficient) of the polynomial obtained by erasing the leading term of `f` is equal to the support set of `f` with the degree of `f` removed. In other words, when you remove the highest degree term from a polynomial, the set of remaining non-zero coefficients corresponds to the original polynomial's support set minus the highest degree.
More concisely: For any polynomial `f` over a semiring `R`, the support sets of `f` and the polynomial obtained by erasing its leading term differ only by the highest degree.
|
Polynomial.eraseLead_monomial
theorem Polynomial.eraseLead_monomial :
∀ {R : Type u_1} [inst : Semiring R] (i : ℕ) (r : R), ((Polynomial.monomial i) r).eraseLead = 0
The theorem `Polynomial.eraseLead_monomial` states that for any semiring `R`, for any natural number `i`, and for any `r` in `R`, when we create a monomial using `r` and `i` in `R`, and then erase the leading term of that monomial, what remains is the zero polynomial. In mathematical terms, if we have a monomial `a * X^s`, erasing the leading term essentially removes the entire monomial, leaving us with the zero polynomial.
More concisely: For any semiring R, erasing the leading term of a monomial a * X^s in R results in the zero polynomial.
|
Polynomial.eraseLead_coeff
theorem Polynomial.eraseLead_coeff :
∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} (i : ℕ),
f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i
The theorem `Polynomial.eraseLead_coeff` states that for any semiring `R`, any polynomial `f` of type `R`, and any natural number `i`, the coefficient of the `i`-th term of the polynomial obtained by erasing the leading term of `f` is determined by a simple rule. If `i` is equal to the degree of the polynomial `f`, then the `i`-th coefficient of the new polynomial is `0`. Otherwise, the `i`-th coefficient of the new polynomial is the same as the `i`-th coefficient of the original polynomial `f`. In other words, the operation of erasing the leading term from a polynomial only affects the coefficient of the term with the highest degree, turning it to `0`, while leaving all other coefficients intact.
More concisely: For any polynomial `f` over a semiring `R` and natural number `i`, the `i`-th coefficient of the polynomial obtained by erasing the leading term of `f` is equal to the `i`-th coefficient of `f` if `i` is not the degree of `f`, and is equal to 0 otherwise.
|
Polynomial.eraseLead_coeff_of_ne
theorem Polynomial.eraseLead_coeff_of_ne :
∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} (i : ℕ),
i ≠ f.natDegree → f.eraseLead.coeff i = f.coeff i
The theorem `Polynomial.eraseLead_coeff_of_ne` states that for any semiring `R`, any polynomial `f` of type `R`, and any natural number `i`, if `i` is not equal to the degree of the polynomial `f` (in other words, `i ≠ Polynomial.natDegree f`), then the coefficient of the `i`-th term of the polynomial obtained by erasing the leading term of `f` (`Polynomial.eraseLead f`) is equal to the coefficient of the `i`-th term of the original polynomial `f`. In mathematical terms, this could be written as: if $i \neq \deg(f)$, then the coefficient of $x^i$ in $f - \text{lead}(f)$ is same as the coefficient of $x^i$ in $f$. Here, $\text{lead}(f)$ denotes the leading term of $f$.
More concisely: If the degree of a polynomial `f` in a semiring `R` does not equal `i`, then the coefficient of `x^i` in `Polynomial.eraseLead f` equals the coefficient of `x^i` in `f`.
|
Polynomial.map_natDegree_eq_sub
theorem Polynomial.map_natDegree_eq_sub :
∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} {F : Type u_3} [inst_1 : Semiring S]
[inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : AddMonoidHomClass F (Polynomial R) (Polynomial S)]
{φ : F} {p : Polynomial R} {k : ℕ},
(∀ (f : Polynomial R), f.natDegree < k → φ f = 0) →
(∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = n - k) →
(φ p).natDegree = p.natDegree - k
The theorem `Polynomial.map_natDegree_eq_sub` states that for any semirings `R` and `S`, a polymorphic function `F` that acts like a function from `Polynomial R` to `Polynomial S`, an additive monoid homomorphism class, a function `φ` of type `F`, a polynomial `p` in `R`, and a natural number `k`, if the function `φ` maps all polynomials of degree less than `k` to 0, and for all natural numbers `n` and coefficients `c` in `R` (that are not zero), the degree of the polynomial obtained by applying `φ` to the monomial `a * X^n` is `n - k`, then the degree of the polynomial obtained by applying `φ` to `p` is equal to the degree of `p` minus `k`. In mathematical notation, the theorem says that if $\phi$ is a function that zeros out all polynomials with degree less than $k$ and shifts the degree of all monomials by $k$, then the degree of $\phi(p)$ is the degree of $p$ minus $k$.
More concisely: Given a semiring homomorphism φ that maps monomials of degree n to monomials of degree n-k and sets polynomials of degree < k to 0, the degree of φ(p) equals the degree of p - k for any polynomial p.
|
Polynomial.mono_map_natDegree_eq
theorem Polynomial.mono_map_natDegree_eq :
∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} {F : Type u_3} [inst_1 : Semiring S]
[inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : AddMonoidHomClass F (Polynomial R) (Polynomial S)]
{φ : F} {p : Polynomial R} (k : ℕ) (fu : ℕ → ℕ),
(∀ {n : ℕ}, n ≤ k → fu n = 0) →
(∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m) →
(∀ {f : Polynomial R}, f.natDegree < k → φ f = 0) →
(∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((Polynomial.monomial n) c)).natDegree = fu n) →
(φ p).natDegree = fu p.natDegree
This theorem states that given a semiring `R`, another semiring `S`, a function `φ` from polynomials over `R` to polynomials over `S`, a natural number `k`, and a function `fu` from natural numbers to natural numbers that is "sufficiently monotone", the following holds:
If `φ` maps all polynomials of degree less than `k` to `0`, and if `φ` maps any monomial of degree `n` in `R[x]` to a polynomial of degree `fu(n)`, then `φ` will map any polynomial `p` in `R[x]` to a polynomial of degree `fu(deg(p))`.
Here, "sufficiently monotone" means that for all natural numbers `n` and `m`, if `n` is greater than or equal to `k` and less than `m`, then `fu(n)` is less than `fu(m)`.
More concisely: Given a semiring homomorphism φ from polynomials over semiring R to polynomials over semiring S, a degree-increasing function fu from natural numbers to natural numbers that is sufficiently monotone, if φ maps all polynomials of degree less than k to 0 and maps each monomial x^n to a polynomial of degree fu(n), then φ maps any polynomial p of degree n in R[x] to a polynomial of degree fu(n) in S[x].
|
Polynomial.eraseLead_zero
theorem Polynomial.eraseLead_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.eraseLead 0 = 0
The theorem `Polynomial.eraseLead_zero` states that for any semiring `R`, the result of applying the `eraseLead` function to the zero polynomial is the zero polynomial. In other words, erasing the leading term of the zero polynomial in any semiring leaves us with the zero polynomial.
More concisely: For any semiring R, the eraseLead function applied to the zero polynomial results in the zero polynomial.
|