Polynomial.revAtFun_eq
theorem Polynomial.revAtFun_eq : ∀ (N i : ℕ), Polynomial.revAtFun N i = (Polynomial.revAt N) i
The theorem `Polynomial.revAtFun_eq` states that for any natural numbers `N` and `i`, the function `Polynomial.revAtFun` applied on `N` and `i` gives the same result as the function `Polynomial.revAt` applied on `N` and then on `i`. This theorem mainly emphasizes the preference of using the bundled version `revAt` over the unbundled version `revAtFun`.
More concisely: For any natural number `N` and index `i`, the functions `Polynomial.revAtFun` and `Polynomial.revAt` applied to `N` and `i` yield equal results.
|
Polynomial.coeff_reverse
theorem Polynomial.coeff_reverse :
∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R) (n : ℕ),
f.reverse.coeff n = f.coeff ((Polynomial.revAt f.natDegree) n)
This theorem states that for any semiring `R`, and for any polynomial `f` over `R` and any natural number `n`, the coefficient of the `n`th term in the reverse of `f` is equal to the coefficient of the term in `f` corresponding to the index obtained by applying the `revAt` function to `n` with `f`'s natural degree as the parameter. In other words, when you reverse a polynomial, the coefficients of the terms are reflected around the "center" which is the natural degree of the polynomial.
More concisely: For any semiring `R`, polynomial `f` over `R` of degree `n`, the coefficient of the `n`th term in the reversed form of `f` equals the coefficient of the term in `f` indexed by `revAt n (degree f)`.
|
Polynomial.revAt_le
theorem Polynomial.revAt_le : ∀ {N i : ℕ}, i ≤ N → (Polynomial.revAt N) i = N - i
The theorem `Polynomial.revAt_le` states that for any natural numbers `N` and `i`, if `i` is less than or equal to `N`, then applying the `Polynomial.revAt` function to `i` (with `N` as the parameter) will result in `N - i`. This theorem essentially confirms the behavior of the `Polynomial.revAt` function for numbers `i` less than or equal to `N`, as stated in the function's definition.
More concisely: For any natural number `N` and `i` less than or equal to `N`, `Polynomial.revAt i N = N - i`.
|
Polynomial.reverse_zero
theorem Polynomial.reverse_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.reverse 0 = 0
This theorem states that for any type `R`, under the assumption that `R` forms a semi-ring, the reverse of the zero polynomial is also the zero polynomial. In other words, "reading backwards" the zero polynomial still gives you the zero polynomial.
More concisely: For any semi-ring `R`, the additive inverse of the zero polynomial is the zero polynomial.
|
Polynomial.reflect_add
theorem Polynomial.reflect_add :
∀ {R : Type u_1} [inst : Semiring R] (f g : Polynomial R) (N : ℕ),
Polynomial.reflect N (f + g) = Polynomial.reflect N f + Polynomial.reflect N g
The theorem `Polynomial.reflect_add` states that for any semiring `R`, any two polynomials `f` and `g` over `R`, and any natural number `N`, the reflection of the sum of `f` and `g` with respect to `N` is equal to the sum of the reflections of `f` and `g` individually with respect to `N`. In other words, the `reflect` operation over polynomials is distributive over addition. This can be expressed mathematically as: for all `f`, `g` in Polynomial `R` and for all `N` in ℕ, `reflect(N, f + g) = reflect(N, f) + reflect(N, g)`, where `reflect` is a function that rearranges the coefficients of a polynomial.
More concisely: For any semiring R, natural number N, and polynomials f and g over R, the reflection of the sum of f and g with respect to N is equal to the sum of the reflections of f and g with respect to N. In other words, the reflection operation over polynomials distributes over polynomial addition.
|
Polynomial.revAt_invol
theorem Polynomial.revAt_invol : ∀ {N i : ℕ}, (Polynomial.revAt N) ((Polynomial.revAt N) i) = i
This theorem states that for all natural numbers `N` and `i`, applying the `Polynomial.revAt N` function twice gives back the original natural number `i`. In other words, the `Polynomial.revAt N` function is an involution, meaning it is its own inverse.
More concisely: For all natural numbers `N` and `i`, `Polynomial.revAt N (Polynomial.revAt N i) = i`.
|
Polynomial.reflect_C_mul_X_pow
theorem Polynomial.reflect_C_mul_X_pow :
∀ {R : Type u_1} [inst : Semiring R] (N n : ℕ) {c : R},
Polynomial.reflect N (Polynomial.C c * Polynomial.X ^ n) =
Polynomial.C c * Polynomial.X ^ (Polynomial.revAt N) n
The theorem `Polynomial.reflect_C_mul_X_pow` states that for any semiring `R`, for any positive integer `N` and `n`, and any constant `c` of type `R`, reflecting the polynomial `c * X^n` (where `X` is the polynomial variable) using `N` is equal to the polynomial `c * X^(revAt N n)`. Here, `revAt` is an operation that returns `N - n` if `n` is less than or equal to `N`, and `n` otherwise. Essentially, this theorem is about reflecting a polynomial that is a product of a constant and a power of the polynomial variable `X`.
More concisely: For any semiring `R`, constant `c` of type `R`, positive integer `N`, and integer `n`, the reflected polynomial `c * X^n` using `N` equals `c * X^(revAt N n)`.
|
Polynomial.coeff_reflect
theorem Polynomial.coeff_reflect :
∀ {R : Type u_1} [inst : Semiring R] (N : ℕ) (f : Polynomial R) (i : ℕ),
(Polynomial.reflect N f).coeff i = f.coeff ((Polynomial.revAt N) i)
This theorem states that for any semiring `R`, any natural number `N`, any polynomial `f` of type `R`, and any natural number `i`, the coefficient of `X^i` in the reflection of `f` about `N` is equal to the coefficient of `X^((N-i) or i)` in `f`. The reflection of `f` about `N` is a new polynomial where the terms of `f` with exponent `[0, ..., N]` now have exponent `[N, ..., 0]`. The function `revAt` returns `N-i` if `i ≤ N`, otherwise it returns `i`.
More concisely: For any semiring `R`, polynomial `f` of type `R`, natural numbers `N` and `i`, the coefficient of `X^(i)` in `f` is equal to the coefficient of `X^(N \|^ i \|^)` in the reflected polynomial `f` about `N`.
|