# 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.

Instances For
theorem Polynomial.revAtFun_invol {N : } {i : } :
= i
def Polynomial.revAt (N : ) :

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.

Instances For
@[simp]
theorem Polynomial.revAtFun_eq (N : ) (i : ) :
= ↑() i

We prefer to use the bundled revAt over unbundled revAtFun.

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

Instances For
theorem Polynomial.reflect_support {R : Type u_1} [] (N : ) (f : ) :
@[simp]
theorem Polynomial.coeff_reflect {R : Type u_1} [] (N : ) (f : ) (i : ) :
= Polynomial.coeff f (↑() i)
@[simp]
theorem Polynomial.reflect_zero {R : Type u_1} [] {N : } :
= 0
@[simp]
theorem Polynomial.reflect_eq_zero_iff {R : Type u_1} [] {N : } {f : } :
= 0 f = 0
@[simp]
theorem Polynomial.reflect_add {R : Type u_1} [] (f : ) (g : ) (N : ) :
@[simp]
theorem Polynomial.reflect_C_mul {R : Type u_1} [] (f : ) (r : R) (N : ) :
Polynomial.reflect N (Polynomial.C r * f) = Polynomial.C r *
theorem Polynomial.reflect_C_mul_X_pow {R : Type u_1} [] (N : ) (n : ) {c : R} :
Polynomial.reflect N (Polynomial.C c * Polynomial.X ^ n) = Polynomial.C c * Polynomial.X ^ ↑() n
@[simp]
theorem Polynomial.reflect_C {R : Type u_1} [] (r : R) (N : ) :
Polynomial.reflect N (Polynomial.C r) = Polynomial.C r * Polynomial.X ^ N
@[simp]
theorem Polynomial.reflect_monomial {R : Type u_1} [] (N : ) (n : ) :
Polynomial.reflect N (Polynomial.X ^ n) = Polynomial.X ^ ↑() n
@[simp]
theorem Polynomial.reflect_one_X {R : Type u_1} [] :
Polynomial.reflect 1 Polynomial.X = 1
theorem Polynomial.reflect_mul_induction {R : Type u_1} [] (cf : ) (cg : ) (N : ) (O : ) (f : ) (g : ) :
Polynomial.reflect (N + O) (f * g) =
@[simp]
theorem Polynomial.reflect_mul {R : Type u_1} [] (f : ) (g : ) {F : } {G : } (Ff : ) (Gg : ) :
Polynomial.reflect (F + G) (f * g) =
theorem Polynomial.eval₂_reflect_mul_pow {R : Type u_1} [] {S : Type u_2} [] (i : R →+* S) (x : S) [] (N : ) (f : ) (hf : ) :
Polynomial.eval₂ i (x) () * x ^ N =
theorem Polynomial.eval₂_reflect_eq_zero_iff {R : Type u_1} [] {S : Type u_2} [] (i : R →+* S) (x : S) [] (N : ) (f : ) (hf : ) :
noncomputable def Polynomial.reverse {R : Type u_1} [] (f : ) :

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.

Instances For
theorem Polynomial.coeff_reverse {R : Type u_1} [] (f : ) (n : ) :
= Polynomial.coeff f (↑() n)
@[simp]
theorem Polynomial.coeff_zero_reverse {R : Type u_1} [] (f : ) :
@[simp]
theorem Polynomial.reverse_zero {R : Type u_1} [] :
@[simp]
theorem Polynomial.reverse_eq_zero {R : Type u_1} [] {f : } :
f = 0
theorem Polynomial.reverse_natDegree_le {R : Type u_1} [] (f : ) :
theorem Polynomial.reverse_natDegree {R : Type u_1} [] (f : ) :
theorem Polynomial.reverse_leadingCoeff {R : Type u_1} [] (f : ) :
theorem Polynomial.reverse_natTrailingDegree {R : Type u_1} [] (f : ) :
theorem Polynomial.reverse_trailingCoeff {R : Type u_1} [] (f : ) :
theorem Polynomial.reverse_mul {R : Type u_1} [] {f : } {g : } (fg : ) :
@[simp]
theorem Polynomial.reverse_mul_of_domain {R : Type u_2} [Ring R] [] (f : ) (g : ) :
theorem Polynomial.trailingCoeff_mul {R : Type u_2} [Ring R] [] (p : ) (q : ) :
@[simp]
theorem Polynomial.coeff_one_reverse {R : Type u_1} [] (f : ) :
@[simp]
theorem Polynomial.reverse_C {R : Type u_1} [] (t : R) :
Polynomial.reverse (Polynomial.C t) = Polynomial.C t
@[simp]
theorem Polynomial.reverse_mul_X {R : Type u_1} [] (p : ) :
Polynomial.reverse (p * Polynomial.X) =
@[simp]
theorem Polynomial.reverse_X_mul {R : Type u_1} [] (p : ) :
Polynomial.reverse (Polynomial.X * p) =
@[simp]
theorem Polynomial.reverse_mul_X_pow {R : Type u_1} [] (p : ) (n : ) :
Polynomial.reverse (p * Polynomial.X ^ n) =
@[simp]
theorem Polynomial.reverse_X_pow_mul {R : Type u_1} [] (p : ) (n : ) :
Polynomial.reverse (Polynomial.X ^ n * p) =
@[simp]
theorem Polynomial.reverse_add_C {R : Type u_1} [] (p : ) (t : R) :
Polynomial.reverse (p + Polynomial.C t) = + Polynomial.C t * Polynomial.X ^
@[simp]
theorem Polynomial.reverse_C_add {R : Type u_1} [] (p : ) (t : R) :
Polynomial.reverse (Polynomial.C t + p) = Polynomial.C t * Polynomial.X ^ +
theorem Polynomial.eval₂_reverse_mul_pow {R : Type u_1} [] {S : Type u_2} [] (i : R →+* S) (x : S) [] (f : ) :
@[simp]
theorem Polynomial.eval₂_reverse_eq_zero_iff {R : Type u_1} [] {S : Type u_2} [] (i : R →+* S) (x : S) [] (f : ) :
@[simp]
theorem Polynomial.reflect_neg {R : Type u_1} [Ring R] (f : ) (N : ) :
=
@[simp]
theorem Polynomial.reflect_sub {R : Type u_1} [Ring R] (f : ) (g : ) (N : ) :
@[simp]
theorem Polynomial.reverse_neg {R : Type u_1} [Ring R] (f : ) :