mathlib documentation

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. We also define polynomial.norm2, which is the sum of the squares of the coefficients of a polynomial. It is also a coefficient of p * p.mirror.

Main definitions #

polynomial.mirror
polynomial.norm2

Main results #

polynomial.mirror_mul_of_domain: mirror preserves multiplication.
polynomial.irreducible_of_mirror: an irreducibility criterion involving mirror
polynomial.norm2_eq_mul_reverse_coeff: norm2 is a coefficient of p * p.mirror

noncomputable def polynomial.mirror {R : Type u_1} [semiring R] (p : R[X]) :

mirror of a polynomial: reverses the coefficients while preserving polynomial.nat_degree

Equations

p.mirror = (p.reverse) * polynomial.X ^ p.nat_trailing_degree

@[simp]

theorem polynomial.mirror_zero {R : Type u_1} [semiring R] :

theorem polynomial.mirror_monomial {R : Type u_1} [semiring R] (n : ℕ) (a : R) :

(⇑(polynomial.monomial n) a).mirror = ⇑(polynomial.monomial n) a

theorem polynomial.mirror_C {R : Type u_1} [semiring R] (a : R) :

(⇑polynomial.C a).mirror = ⇑polynomial.C a

theorem polynomial.mirror_X {R : Type u_1} [semiring R] :

polynomial.X.mirror = polynomial.X

theorem polynomial.mirror_nat_degree {R : Type u_1} [semiring R] (p : R[X]) :

p.mirror.nat_degree = p.nat_degree

theorem polynomial.mirror_nat_trailing_degree {R : Type u_1} [semiring R] (p : R[X]) :

p.mirror.nat_trailing_degree = p.nat_trailing_degree

theorem polynomial.coeff_mirror {R : Type u_1} [semiring R] (p : R[X]) (n : ℕ) :

p.mirror.coeff n = p.coeff (⇑(polynomial.rev_at (p.nat_degree + p.nat_trailing_degree)) n)

theorem polynomial.mirror_eval_one {R : Type u_1} [semiring R] (p : R[X]) :

polynomial.eval 1 p.mirror = polynomial.eval 1 p

theorem polynomial.mirror_mirror {R : Type u_1} [semiring R] (p : R[X]) :

p.mirror.mirror = p

theorem polynomial.mirror_eq_zero {R : Type u_1} [semiring R] (p : R[X]) :

p.mirror = 0 ↔ p = 0

theorem polynomial.mirror_trailing_coeff {R : Type u_1} [semiring R] (p : R[X]) :

p.mirror.trailing_coeff = p.leading_coeff

theorem polynomial.mirror_leading_coeff {R : Type u_1} [semiring R] (p : R[X]) :

p.mirror.leading_coeff = p.trailing_coeff

theorem polynomial.mirror_mul_of_domain {R : Type u_1} [ring R] [is_domain R] (p q : R[X]) :

(p * q).mirror = (p.mirror) * q.mirror

theorem polynomial.mirror_smul {R : Type u_1} [ring R] [is_domain R] (p : R[X]) (a : R) :

(a • p).mirror = a • p.mirror

theorem polynomial.mirror_neg {R : Type u_1} [ring R] (p : R[X]) :

(-p).mirror = -p.mirror

theorem polynomial.irreducible_of_mirror {R : Type u_1} [comm_ring R] [is_domain R] {f : R[X]} (h1 : ¬is_unit f) (h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror) (h3 : ∀ (g : R[X]), g ∣ f → g ∣ f.mirror → is_unit g) :