mathlib3 documentation

data.polynomial.mirror

"Mirror" of a univariate polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

noncomputable 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_mirror {R : Type u_1} [semiring R] (p : polynomial R) :
theorem polynomial.mirror_eq_iff {R : Type u_1} [semiring R] {p q : polynomial R} :
p.mirror = q p = q.mirror
@[simp]
theorem polynomial.mirror_inj {R : Type u_1} [semiring R] {p q : polynomial R} :
p.mirror = q.mirror p = q
@[simp]
theorem polynomial.mirror_eq_zero {R : Type u_1} [semiring R] {p : polynomial R} :
p.mirror = 0 p = 0
theorem polynomial.coeff_mul_mirror {R : Type u_1} [semiring R] (p : polynomial R) :
(p * p.mirror).coeff (p.nat_degree + p.nat_trailing_degree) = p.sum (λ (n : ), λ (_x : R), _x ^ 2)
theorem polynomial.mirror_neg {R : Type u_1} [ring R] (p : polynomial R) :
theorem polynomial.mirror_mul_of_domain {R : Type u_1} [ring R] (p q : polynomial R) [no_zero_divisors R] :
(p * q).mirror = p.mirror * q.mirror
theorem polynomial.mirror_smul {R : Type u_1} [ring R] (p : polynomial R) [no_zero_divisors R] (a : R) :
(a p).mirror = a p.mirror
theorem polynomial.irreducible_of_mirror {R : Type u_1} [comm_ring R] [no_zero_divisors R] {f : polynomial R} (h1 : ¬is_unit f) (h2 : (k : polynomial R), f * f.mirror = k * k.mirror k = f k = -f k = f.mirror k = -f.mirror) (h3 : (g : polynomial R), g f g f.mirror is_unit g) :