# Documentation

Mathlib.Data.Polynomial.Mirror

# "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 #

• 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} [] (p : ) :

mirror of a polynomial: reverses the coefficients while preserving Polynomial.natDegree

Instances For
@[simp]
theorem Polynomial.mirror_zero {R : Type u_1} [] :
theorem Polynomial.mirror_monomial {R : Type u_1} [] (n : ) (a : R) :
Polynomial.mirror (↑() a) = ↑() a
theorem Polynomial.mirror_C {R : Type u_1} [] (a : R) :
Polynomial.mirror (Polynomial.C a) = Polynomial.C a
theorem Polynomial.mirror_X {R : Type u_1} [] :
Polynomial.mirror Polynomial.X = Polynomial.X
theorem Polynomial.mirror_natDegree {R : Type u_1} [] (p : ) :
theorem Polynomial.mirror_natTrailingDegree {R : Type u_1} [] (p : ) :
theorem Polynomial.coeff_mirror {R : Type u_1} [] (p : ) (n : ) :
theorem Polynomial.mirror_eval_one {R : Type u_1} [] (p : ) :
theorem Polynomial.mirror_mirror {R : Type u_1} [] (p : ) :
theorem Polynomial.mirror_involutive {R : Type u_1} [] :
Function.Involutive Polynomial.mirror
theorem Polynomial.mirror_eq_iff {R : Type u_1} [] {p : } {q : } :
@[simp]
theorem Polynomial.mirror_inj {R : Type u_1} [] {p : } {q : } :
p = q
@[simp]
theorem Polynomial.mirror_eq_zero {R : Type u_1} [] {p : } :
p = 0
@[simp]
theorem Polynomial.mirror_trailingCoeff {R : Type u_1} [] (p : ) :
@[simp]
theorem Polynomial.mirror_leadingCoeff {R : Type u_1} [] (p : ) :
theorem Polynomial.coeff_mul_mirror {R : Type u_1} [] (p : ) :
= Polynomial.sum p fun n x => x ^ 2
theorem Polynomial.natDegree_mul_mirror {R : Type u_1} [] (p : ) [] :
theorem Polynomial.natTrailingDegree_mul_mirror {R : Type u_1} [] (p : ) [] :
theorem Polynomial.mirror_neg {R : Type u_1} [Ring R] (p : ) :
theorem Polynomial.mirror_mul_of_domain {R : Type u_1} [Ring R] (p : ) (q : ) [] :
theorem Polynomial.mirror_smul {R : Type u_1} [Ring R] (p : ) [] (a : R) :
theorem Polynomial.irreducible_of_mirror {R : Type u_1} [] [] {f : } (h1 : ¬) (h2 : ∀ (k : ), = k = f k = -f ) (h3 : ∀ (g : ), g f) :