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 #

Main results #

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

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

Equations
@[simp]
theorem polynomial.mirror_zero {R : Type u_1} [semiring R] :
0.mirror = 0
theorem polynomial.mirror_monomial {R : Type u_1} [semiring R] (n : ) (a : R) :
theorem polynomial.mirror_C {R : Type u_1} [semiring R] (a : R) :
theorem polynomial.mirror_mirror {R : Type u_1} [semiring R] (p : polynomial R) :
theorem polynomial.mirror_eq_zero {R : Type u_1} [semiring R] (p : polynomial R) :
p.mirror = 0 p = 0
theorem polynomial.mirror_mul_of_domain {R : Type u_1} [integral_domain R] (p q : polynomial R) :
(p * q).mirror = (p.mirror) * q.mirror
theorem polynomial.mirror_smul {R : Type u_1} [integral_domain R] (p : polynomial R) (a : R) :
(a p).mirror = a p.mirror
theorem polynomial.mirror_neg {R : Type u_1} [ring R] (p : polynomial R) :
theorem polynomial.irreducible_of_mirror {R : Type u_1} [integral_domain R] {f : polynomial R} (h1 : ¬is_unit f) (h2 : ∀ (k : polynomial R), f * f.mirror = k * k.mirrork = f k = -f k = f.mirror k = -f.mirror) (h3 : ∀ (g : polynomial R), g fg f.mirroris_unit g) :