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
🔸 coverage
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

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