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