# mathlib3documentation

data.polynomial.mirror

# "Mirror" of a univariate polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• polynomial.mirror

## Main results #

• polynomial.mirror_mul_of_domain: mirror preserves multiplication.
• polynomial.irreducible_of_mirror: an irreducibility criterion involving mirror
noncomputable def polynomial.mirror {R : Type u_1} [semiring R] (p : polynomial R) :

mirror of a polynomial: reverses the coefficients while preserving polynomial.nat_degree

Equations
@[simp]
theorem polynomial.mirror_zero {R : Type u_1} [semiring R] :
0.mirror = 0
theorem polynomial.mirror_monomial {R : Type u_1} [semiring R] (n : ) (a : R) :
( a).mirror = a
theorem polynomial.mirror_C {R : Type u_1} [semiring R] (a : R) :
theorem polynomial.mirror_X {R : Type u_1} [semiring R] :
theorem polynomial.mirror_nat_degree {R : Type u_1} [semiring R] (p : polynomial R) :
theorem polynomial.coeff_mirror {R : Type u_1} [semiring R] (p : polynomial R) (n : ) :
p.mirror.coeff n = p.coeff ( n)
theorem polynomial.mirror_eval_one {R : Type u_1} [semiring R] (p : polynomial R) :
theorem polynomial.mirror_mirror {R : Type u_1} [semiring R] (p : polynomial R) :
theorem polynomial.mirror_eq_iff {R : Type u_1} [semiring R] {p q : polynomial R} :
p.mirror = q p = q.mirror
@[simp]
theorem polynomial.mirror_inj {R : Type u_1} [semiring R] {p q : polynomial R} :
p.mirror = q.mirror p = q
@[simp]
theorem polynomial.mirror_eq_zero {R : Type u_1} [semiring R] {p : polynomial R} :
p.mirror = 0 p = 0
@[simp]
theorem polynomial.mirror_trailing_coeff {R : Type u_1} [semiring R] (p : polynomial R) :
@[simp]
theorem polynomial.mirror_leading_coeff {R : Type u_1} [semiring R] (p : polynomial R) :
theorem polynomial.coeff_mul_mirror {R : Type u_1} [semiring R] (p : polynomial R) :
(p * p.mirror).coeff = p.sum (λ (n : ), λ (_x : R), _x ^ 2)
theorem polynomial.mirror_neg {R : Type u_1} [ring R] (p : polynomial R) :
theorem polynomial.mirror_mul_of_domain {R : Type u_1} [ring R] (p q : polynomial R)  :
(p * q).mirror = p.mirror * q.mirror
theorem polynomial.mirror_smul {R : Type u_1} [ring R] (p : polynomial R) (a : R) :
(a p).mirror = a p.mirror
theorem polynomial.irreducible_of_mirror {R : Type u_1} [comm_ring R] {f : polynomial R} (h1 : ¬) (h2 : (k : , f * f.mirror = k * k.mirror k = f k = -f k = f.mirror k = -f.mirror) (h3 : (g : , g f g f.mirror ) :