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

noncomputable def Polynomial.mirror {R : Type u_1} [Semiring R] (p : Polynomial R) :

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

Instances For
    theorem Polynomial.mirror_C {R : Type u_1} [Semiring R] (a : R) :
    Polynomial.mirror (Polynomial.C a) = Polynomial.C a
    theorem Polynomial.mirror_X {R : Type u_1} [Semiring R] :
    Polynomial.mirror Polynomial.X = Polynomial.X
    theorem Polynomial.mirror_involutive {R : Type u_1} [Semiring R] :
    Function.Involutive Polynomial.mirror
    theorem Polynomial.mirror_eq_zero {R : Type u_1} [Semiring R] {p : Polynomial R} :
    theorem Polynomial.irreducible_of_mirror {R : Type u_1} [CommRing R] [NoZeroDivisors R] {f : Polynomial R} (h1 : ¬IsUnit f) (h2 : ∀ (k : Polynomial R), f * Polynomial.mirror f = k * Polynomial.mirror kk = f k = -f k = Polynomial.mirror f k = -Polynomial.mirror f) (h3 : ∀ (g : Polynomial R), g fg Polynomial.mirror fIsUnit g) :