Polynomial.mirror_natTrailingDegree
theorem Polynomial.mirror_natTrailingDegree :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.natTrailingDegree = p.natTrailingDegree := by
sorry
This theorem states that for any semiring `R` and any polynomial `p` over `R`, the natural trailing degree of the mirror of the polynomial `p` is equal to the natural trailing degree of `p` itself. Here, the mirror of a polynomial is defined as the polynomial obtained by reversing the coefficients of `p` and then multiplying by `X` to the power of the natural trailing degree of `p`. The natural trailing degree of a polynomial is the lowest degree of its non-zero terms, with the convention that the natural trailing degree of the zero polynomial is zero.
More concisely: For any semiring `R` and polynomial `p` over `R`, the natural trailing degrees of `p` and its mirror are equal.
|
Polynomial.mirror_zero
theorem Polynomial.mirror_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.mirror 0 = 0
The theorem `Polynomial.mirror_zero` states that for all semirings `R`, the mirror of the zero polynomial is zero. Here, the mirror of a polynomial is defined as the polynomial obtained by reversing the coefficients of the original polynomial and adjusting by multiplying with `X` raised to the power of the natural trailing degree of the original polynomial.
More concisely: For all semirings R, the mirror of the zero polynomial is the polynomial with all coefficients equal to 0.
|
Polynomial.mirror_mirror
theorem Polynomial.mirror_mirror : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.mirror = p := by
sorry
The theorem `Polynomial.mirror_mirror` states that for any type `R` that is a semiring, and a polynomial `p` from that semiring, if we apply the "mirror" operation twice, we get back the original polynomial. In other words, mirroring a polynomial is an involution in the semiring of polynomials over `R`. The "mirror" of a polynomial is defined as the product of the reversed polynomial and `X` raised to the power of the natural trailing degree of the polynomial.
More concisely: For any semiring `R` and polynomial `p` over `R`, applying the mirror operation twice equals the identity on `p`, where the mirror operation is defined as the reversed polynomial multiplied by `X` raised to the power of the degree of `p`.
|
Polynomial.mirror_natDegree
theorem Polynomial.mirror_natDegree :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.natDegree = p.natDegree
This theorem states that for any given polynomial `p` in a semiring `R`, the natural degree of the mirror of `p` is equal to the natural degree of `p` itself. In other words, the operation of mirroring, which reverses the coefficients of the polynomial while preserving its natural degree, doesn't change the natural degree of the polynomial.
More concisely: For any polynomial `p` in a semiring `R`, the natural degree of the mirrored polynomial is equal to the natural degree of `p`.
|
Polynomial.coeff_mirror
theorem Polynomial.coeff_mirror :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
p.mirror.coeff n = p.coeff ((Polynomial.revAt (p.natDegree + p.natTrailingDegree)) n)
The theorem `Polynomial.coeff_mirror` states that for all semiring `R` and any polynomial `p` of type `R`, the coefficient of the `n`-th term of the mirror of `p` is equal to the coefficient of the term corresponding to `revAt (natDegree p + natTrailingDegree p)` of `p`. Here, `Polynomial.mirror p` refers to the polynomial obtained by reversing the coefficients of `p` while preserving its degree, `Polynomial.revAt N` is an involution that returns `N - i` if `i ≤ N` and `i` otherwise, and `natDegree` and `natTrailingDegree` are the degree and trailing degree of the polynomial forced to ℕ, respectively.
More concisely: For any polynomial `p` over a semiring `R`, the coefficient of the `n`-th term of `p`'s mirror is equal to the coefficient of the term at position `natDegree p + natTrailingDegree p - n` in `p`.
|