Documentation

Mathlib.Data.Polynomial.Reverse

Reverse of a univariate polynomial #

The main definition is reverse. Applying reverse to a polynomial f : R[X] produces the polynomial with a reversed list of coefficients, equivalent to X^f.natDegree * f(1/X).

The main result is that reverse (f * g) = reverse f * reverse g, provided the leading coefficients of f and g do not multiply to zero.

def Polynomial.revAtFun (N : ) (i : ) :

If i ≤ N, then revAtFun N i returns N - i, otherwise it returns i. This is the map used by the embedding revAt.

Equations
Instances For

    If i ≤ N, then revAt N i returns N - i, otherwise it returns i. Essentially, this embedding is only used for i ≤ N. The advantage of revAt N i over N - i is that revAt is an involution.

    Equations
    Instances For
      @[simp]

      We prefer to use the bundled revAt over unbundled revAtFun.

      @[simp]
      theorem Polynomial.revAt_invol {N : } {i : } :
      ↑(Polynomial.revAt N) (↑(Polynomial.revAt N) i) = i
      @[simp]
      theorem Polynomial.revAt_le {N : } {i : } (H : i N) :
      ↑(Polynomial.revAt N) i = N - i
      theorem Polynomial.revAt_eq_self_of_lt {N : } {i : } (h : N < i) :
      ↑(Polynomial.revAt N) i = i
      theorem Polynomial.revAt_add {N : } {O : } {n : } {o : } (hn : n N) (ho : o O) :
      ↑(Polynomial.revAt (N + O)) (n + o) = ↑(Polynomial.revAt N) n + ↑(Polynomial.revAt O) o
      noncomputable def Polynomial.reflect {R : Type u_1} [Semiring R] (N : ) :

      reflect N f is the polynomial such that (reflect N f).coeff i = f.coeff (revAt N i). In other words, the terms with exponent [0, ..., N] now have exponent [N, ..., 0].

      In practice, reflect is only used when N is at least as large as the degree of f.

      Eventually, it will be used with N exactly equal to the degree of f.

      Equations
      Instances For
        @[simp]
        theorem Polynomial.reflect_zero {R : Type u_1} [Semiring R] {N : } :
        @[simp]
        theorem Polynomial.reflect_eq_zero_iff {R : Type u_1} [Semiring R] {N : } {f : Polynomial R} :
        @[simp]
        @[simp]
        theorem Polynomial.reflect_C_mul {R : Type u_1} [Semiring R] (f : Polynomial R) (r : R) (N : ) :
        Polynomial.reflect N (Polynomial.C r * f) = Polynomial.C r * Polynomial.reflect N f
        theorem Polynomial.reflect_C_mul_X_pow {R : Type u_1} [Semiring R] (N : ) (n : ) {c : R} :
        Polynomial.reflect N (Polynomial.C c * Polynomial.X ^ n) = Polynomial.C c * Polynomial.X ^ ↑(Polynomial.revAt N) n
        @[simp]
        theorem Polynomial.reflect_C {R : Type u_1} [Semiring R] (r : R) (N : ) :
        Polynomial.reflect N (Polynomial.C r) = Polynomial.C r * Polynomial.X ^ N
        @[simp]
        theorem Polynomial.reflect_monomial {R : Type u_1} [Semiring R] (N : ) (n : ) :
        Polynomial.reflect N (Polynomial.X ^ n) = Polynomial.X ^ ↑(Polynomial.revAt N) n
        @[simp]
        theorem Polynomial.reflect_one_X {R : Type u_1} [Semiring R] :
        Polynomial.reflect 1 Polynomial.X = 1
        @[simp]
        theorem Polynomial.reflect_mul {R : Type u_1} [Semiring R] (f : Polynomial R) (g : Polynomial R) {F : } {G : } (Ff : Polynomial.natDegree f F) (Gg : Polynomial.natDegree g G) :
        theorem Polynomial.eval₂_reflect_mul_pow {R : Type u_1} [Semiring R] {S : Type u_2} [CommSemiring S] (i : R →+* S) (x : S) [Invertible x] (N : ) (f : Polynomial R) (hf : Polynomial.natDegree f N) :
        noncomputable def Polynomial.reverse {R : Type u_1} [Semiring R] (f : Polynomial R) :

        The reverse of a polynomial f is the polynomial obtained by "reading f backwards". Even though this is not the actual definition, reverse f = f (1/X) * X ^ f.natDegree.

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem Polynomial.reverse_C {R : Type u_1} [Semiring R] (t : R) :
          Polynomial.reverse (Polynomial.C t) = Polynomial.C t
          @[simp]
          theorem Polynomial.reverse_mul_X {R : Type u_1} [Semiring R] (p : Polynomial R) :
          @[simp]
          theorem Polynomial.reverse_X_mul {R : Type u_1} [Semiring R] (p : Polynomial R) :
          @[simp]
          theorem Polynomial.reverse_mul_X_pow {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ) :
          @[simp]
          theorem Polynomial.reverse_X_pow_mul {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ) :
          @[simp]
          theorem Polynomial.reverse_add_C {R : Type u_1} [Semiring R] (p : Polynomial R) (t : R) :
          Polynomial.reverse (p + Polynomial.C t) = Polynomial.reverse p + Polynomial.C t * Polynomial.X ^ Polynomial.natDegree p
          @[simp]
          theorem Polynomial.reverse_C_add {R : Type u_1} [Semiring R] (p : Polynomial R) (t : R) :
          Polynomial.reverse (Polynomial.C t + p) = Polynomial.C t * Polynomial.X ^ Polynomial.natDegree p + Polynomial.reverse p
          @[simp]
          @[simp]
          @[simp]