Reverse of a univariate polynomial #
The main definition is
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
g do not multiply to zero.
i ≤ N, then
rev_at N i returns
N - i, otherwise it returns
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.
reflect is only used when
N is at least as large as the degree of
Eventually, it will be used with
N exactly equal to the degree of
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.