# mathlibdocumentation

data.polynomial.reverse

# Reverse of a univariate polynomial #

The main definition is reverse. Applying reverse to a polynomial f : polynomial R produces the polynomial with a reversed list of coefficients, equivalent to X^f.nat_degree * 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.rev_at_fun (N i : ) :

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

Equations
def polynomial.rev_at (N : ) :

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

Equations
@[simp]
theorem polynomial.rev_at_fun_eq (N i : ) :
= i

We prefer to use the bundled rev_at over unbundled rev_at_fun.

@[simp]
theorem polynomial.rev_at_invol {N i : } :
( i) = i
@[simp]
theorem polynomial.rev_at_le {N i : } (H : i N) :
i = N - i
theorem polynomial.rev_at_add {N O n o : } (hn : n N) (ho : o O) :
(polynomial.rev_at (N + O)) (n + o) = n + o
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 (rev_at 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
theorem polynomial.reflect_support {R : Type u_1} [semiring R] (N : ) (f : polynomial R) :
@[simp]
theorem polynomial.coeff_reflect {R : Type u_1} [semiring R] (N : ) (f : polynomial R) (i : ) :
f).coeff i = f.coeff ( i)
@[simp]
theorem polynomial.reflect_zero {R : Type u_1} [semiring R] {N : } :
= 0
@[simp]
theorem polynomial.reflect_eq_zero_iff {R : Type u_1} [semiring R] {N : } {f : polynomial R} :
= 0 f = 0
@[simp]
theorem polynomial.reflect_add {R : Type u_1} [semiring R] (f g : polynomial R) (N : ) :
(f + g) =
@[simp]
theorem polynomial.reflect_C_mul {R : Type u_1} [semiring R] (f : polynomial R) (r : R) (N : ) :
((polynomial.C r) * f) = *
@[simp]
theorem polynomial.reflect_C_mul_X_pow {R : Type u_1} [semiring R] (N n : ) {c : R} :
@[simp]
theorem polynomial.reflect_monomial {R : Type u_1} [semiring R] (N n : ) :
=
theorem polynomial.reflect_mul_induction {R : Type u_1} [semiring R] (cf cg N O : ) (f g : polynomial R) :
f.support.card cf.succg.support.card cg.succf.nat_degree Ng.nat_degree Opolynomial.reflect (N + O) (f * g) = f) *
@[simp]
theorem polynomial.reflect_mul {R : Type u_1} [semiring R] (f g : polynomial R) {F G : } (Ff : f.nat_degree F) (Gg : g.nat_degree G) :
polynomial.reflect (F + G) (f * g) = f) *
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.nat_degree.

Equations
theorem polynomial.coeff_reverse {R : Type u_1} [semiring R] (f : polynomial R) (n : ) :
f.reverse.coeff n = f.coeff n)
@[simp]
theorem polynomial.coeff_zero_reverse {R : Type u_1} [semiring R] (f : polynomial R) :
@[simp]
theorem polynomial.reverse_zero {R : Type u_1} [semiring R] :
@[simp]
theorem polynomial.reverse_eq_zero {R : Type u_1} [semiring R] {f : polynomial R} :
f.reverse = 0 f = 0
theorem polynomial.reverse_nat_degree_le {R : Type u_1} [semiring R] (f : polynomial R) :
theorem polynomial.reverse_nat_degree {R : Type u_1} [semiring R] (f : polynomial R) :
theorem polynomial.reverse_leading_coeff {R : Type u_1} [semiring R] (f : polynomial R) :
theorem polynomial.reverse_nat_trailing_degree {R : Type u_1} [semiring R] (f : polynomial R) :
theorem polynomial.reverse_trailing_coeff {R : Type u_1} [semiring R] (f : polynomial R) :
theorem polynomial.reverse_mul {R : Type u_1} [semiring R] {f g : polynomial R} (fg : 0) :
(f * g).reverse = (f.reverse) * g.reverse
@[simp]
theorem polynomial.reverse_mul_of_domain {R : Type u_1} [domain R] (f g : polynomial R) :
(f * g).reverse = (f.reverse) * g.reverse
theorem polynomial.trailing_coeff_mul {R : Type u_1} (p q : polynomial R) :
@[simp]
theorem polynomial.coeff_one_reverse {R : Type u_1} [semiring R] (f : polynomial R) :
@[simp]
theorem polynomial.reflect_neg {R : Type u_1} [ring R] (f : polynomial R) (N : ) :
(-f) =
@[simp]
theorem polynomial.reflect_sub {R : Type u_1} [ring R] (f g : polynomial R) (N : ) :
(f - g) =
@[simp]
theorem polynomial.reverse_neg {R : Type u_1} [ring R] (f : polynomial R) :