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 #

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.nat_degree

Equations
source
@[simp]
theorem polynomial.mirror_zero {R : Type u_1} [semiring R] :
0.mirror = 0
source
theorem polynomial.mirror_monomial {R : Type u_1} [semiring R] (n : ℕ) (a : R) :
(⇑(polynomial.monomial n) a).mirror = ⇑(polynomial.monomial n) a
source
theorem polynomial.mirror_C {R : Type u_1} [semiring R] (a : R) :
(⇑polynomial.C a).mirror = ⇑polynomial.C a
source
theorem polynomial.mirror_X {R : Type u_1} [semiring R] :
polynomial.X.mirror = polynomial.X
source
theorem polynomial.mirror_nat_degree {R : Type u_1} [semiring R] (p : polynomial R) :
p.mirror.nat_degree = p.nat_degree
source
theorem polynomial.mirror_nat_trailing_degree {R : Type u_1} [semiring R] (p : polynomial R) :
p.mirror.nat_trailing_degree = p.nat_trailing_degree
source
theorem polynomial.coeff_mirror {R : Type u_1} [semiring R] (p : polynomial R) (n : ℕ) :
p.mirror.coeff n = p.coeff (⇑(polynomial.rev_at (p.nat_degree + p.nat_trailing_degree)) n)
source
theorem polynomial.mirror_eval_one {R : Type u_1} [semiring R] (p : polynomial R) :
polynomial.eval 1 p.mirror = polynomial.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 polynomial.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_trailing_coeff {R : Type u_1} [semiring R] (p : polynomial R) :
p.mirror.trailing_coeff = p.leading_coeff
source
@[simp]
theorem polynomial.mirror_leading_coeff {R : Type u_1} [semiring R] (p : polynomial R) :
p.mirror.leading_coeff = p.trailing_coeff
source
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)
source
theorem polynomial.nat_degree_mul_mirror {R : Type u_1} [semiring R] (p : polynomial R) [no_zero_divisors R] :
(p * p.mirror).nat_degree = 2 * p.nat_degree
source
theorem polynomial.nat_trailing_degree_mul_mirror {R : Type u_1} [semiring R] (p : polynomial R) [no_zero_divisors R] :
(p * p.mirror).nat_trailing_degree = 2 * p.nat_trailing_degree
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) [no_zero_divisors R] :
(p * q).mirror = p.mirror * q.mirror
source
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
source
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) :
irreducible f