"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
.
Main definitions #
Main results #
polynomial.mirror_mul_of_domain
:mirror
preserves multiplication.polynomial.irreducible_of_mirror
: an irreducibility criterion involvingmirror
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 : polynomial R) :
p.mirror.nat_degree = p.nat_degree
theorem
polynomial.coeff_mirror
{R : Type u_1}
[semiring R]
(p : polynomial R)
(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 : polynomial R) :
polynomial.eval 1 p.mirror = polynomial.eval 1 p
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.coeff_mul_mirror
{R : Type u_1}
[semiring R]
(p : polynomial R) :
(p * p.mirror).coeff (p.nat_degree + p.nat_trailing_degree) = p.sum (λ (n : ℕ), λ (_x : R), _x ^ 2)
theorem
polynomial.nat_degree_mul_mirror
{R : Type u_1}
[semiring R]
(p : polynomial R)
[no_zero_divisors R] :
(p * p.mirror).nat_degree = 2 * p.nat_degree
theorem
polynomial.nat_trailing_degree_mul_mirror
{R : Type u_1}
[semiring R]
(p : polynomial R)
[no_zero_divisors R] :
(p * p.mirror).nat_trailing_degree = 2 * p.nat_trailing_degree
theorem
polynomial.mirror_mul_of_domain
{R : Type u_1}
[ring R]
(p q : polynomial R)
[no_zero_divisors R] :
theorem
polynomial.mirror_smul
{R : Type u_1}
[ring R]
(p : polynomial R)
[no_zero_divisors R]
(a : R) :