"Mirror" of a univariate polynomial #
In this file we define polynomial.mirror
, a variant of polynomial.reverse
. The difference
between reverse
and mirror
is that reverse
will decrease the degree if the polynomial is
divisible by X
. We also define polynomial.norm2
, which is the sum of the squares of the
coefficients of a polynomial. It is also a coefficient of p * p.mirror
.
Main definitions #
polynomial.mirror
polynomial.norm2
Main results #
polynomial.mirror_mul_of_domain
:mirror
preserves multiplication.polynomial.irreducible_of_mirror
: an irreducibility criterion involvingmirror
polynomial.norm2_eq_mul_reverse_coeff
:norm2
is a coefficient ofp * p.mirror
mirror of a polynomial: reverses the coefficients while preserving polynomial.nat_degree
Equations
- p.mirror = (p.reverse) * polynomial.X ^ p.nat_trailing_degree
theorem
polynomial.mirror_monomial
{R : Type u_1}
[semiring R]
(n : ℕ)
(a : R) :
(⇑(polynomial.monomial n) a).mirror = ⇑(polynomial.monomial n) a
theorem
polynomial.mirror_C
{R : Type u_1}
[semiring R]
(a : R) :
(⇑polynomial.C a).mirror = ⇑polynomial.C a
theorem
polynomial.mirror_nat_degree
{R : Type u_1}
[semiring R]
(p : R[X]) :
p.mirror.nat_degree = p.nat_degree
theorem
polynomial.coeff_mirror
{R : Type u_1}
[semiring R]
(p : R[X])
(n : ℕ) :
p.mirror.coeff n = p.coeff (⇑(polynomial.rev_at (p.nat_degree + p.nat_trailing_degree)) n)
theorem
polynomial.mirror_eval_one
{R : Type u_1}
[semiring R]
(p : R[X]) :
polynomial.eval 1 p.mirror = polynomial.eval 1 p