Documentation

Mathlib.Algebra.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 #

Main results #

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

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

Equations
Instances For
    source
    @[simp]
    theorem Polynomial.mirror_zero {R : Type u_1} [Semiring R] :
    Polynomial.mirror 0 = 0
    source
    theorem Polynomial.mirror_monomial {R : Type u_1} [Semiring R] (n : ℕ) (a : R) :
    Polynomial.mirror ((Polynomial.monomial n) a) = (Polynomial.monomial n) a
    source
    theorem Polynomial.mirror_C {R : Type u_1} [Semiring R] (a : R) :
    Polynomial.mirror (Polynomial.C a) = Polynomial.C a
    source
    theorem Polynomial.mirror_X {R : Type u_1} [Semiring R] :
    Polynomial.mirror Polynomial.X = Polynomial.X
    source
    theorem Polynomial.mirror_natDegree {R : Type u_1} [Semiring R] (p : Polynomial R) :
    Polynomial.natDegree (Polynomial.mirror p) = Polynomial.natDegree p
    source
    theorem Polynomial.mirror_natTrailingDegree {R : Type u_1} [Semiring R] (p : Polynomial R) :
    Polynomial.natTrailingDegree (Polynomial.mirror p) = Polynomial.natTrailingDegree p
    source
    theorem Polynomial.coeff_mirror {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) :
    Polynomial.coeff (Polynomial.mirror p) n = Polynomial.coeff p ((Polynomial.revAt (Polynomial.natDegree p + Polynomial.natTrailingDegree p)) n)
    source
    theorem Polynomial.mirror_eval_one {R : Type u_1} [Semiring R] (p : Polynomial R) :
    Polynomial.eval 1 (Polynomial.mirror p) = Polynomial.eval 1 p
    source
    theorem Polynomial.mirror_mirror {R : Type u_1} [Semiring R] (p : Polynomial R) :
    Polynomial.mirror (Polynomial.mirror p) = p
    source
    theorem Polynomial.mirror_involutive {R : Type u_1} [Semiring R] :
    Function.Involutive Polynomial.mirror
    source
    theorem Polynomial.mirror_eq_iff {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
    Polynomial.mirror p = q ↔ p = Polynomial.mirror q
    source
    @[simp]
    theorem Polynomial.mirror_inj {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} :
    Polynomial.mirror p = Polynomial.mirror q ↔ p = q
    source
    @[simp]
    theorem Polynomial.mirror_eq_zero {R : Type u_1} [Semiring R] {p : Polynomial R} :
    Polynomial.mirror p = 0 ↔ p = 0
    source
    @[simp]
    theorem Polynomial.mirror_trailingCoeff {R : Type u_1} [Semiring R] (p : Polynomial R) :
    Polynomial.trailingCoeff (Polynomial.mirror p) = Polynomial.leadingCoeff p
    source
    @[simp]
    theorem Polynomial.mirror_leadingCoeff {R : Type u_1} [Semiring R] (p : Polynomial R) :
    Polynomial.leadingCoeff (Polynomial.mirror p) = Polynomial.trailingCoeff p
    source
    theorem Polynomial.coeff_mul_mirror {R : Type u_1} [Semiring R] (p : Polynomial R) :
    Polynomial.coeff (p * Polynomial.mirror p) (Polynomial.natDegree p + Polynomial.natTrailingDegree p) = Polynomial.sum p fun (n : ℕ) (x : R) => x ^ 2
    source
    theorem Polynomial.natDegree_mul_mirror {R : Type u_1} [Semiring R] (p : Polynomial R) [NoZeroDivisors R] :
    Polynomial.natDegree (p * Polynomial.mirror p) = 2 * Polynomial.natDegree p
    source
    theorem Polynomial.natTrailingDegree_mul_mirror {R : Type u_1} [Semiring R] (p : Polynomial R) [NoZeroDivisors R] :
    Polynomial.natTrailingDegree (p * Polynomial.mirror p) = 2 * Polynomial.natTrailingDegree p
    source
    theorem Polynomial.mirror_neg {R : Type u_1} [Ring R] (p : Polynomial R) :
    Polynomial.mirror (-p) = -Polynomial.mirror p
    source
    theorem Polynomial.mirror_mul_of_domain {R : Type u_1} [Ring R] (p : Polynomial R) (q : Polynomial R) [NoZeroDivisors R] :
    Polynomial.mirror (p * q) = Polynomial.mirror p * Polynomial.mirror q
    source
    theorem Polynomial.mirror_smul {R : Type u_1} [Ring R] (p : Polynomial R) [NoZeroDivisors R] (a : R) :
    Polynomial.mirror (a • p) = a • Polynomial.mirror p
    source
    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 k → k = f ∨ k = -f ∨ k = Polynomial.mirror f ∨ k = -Polynomial.mirror f) (h3 : IsRelPrime f (Polynomial.mirror f)) :
    Irreducible f