mathlib documentation

data.polynomial.reverse

Reverse of a univariate polynomial #

The main definition is reverse. Applying reverse to a polynomial f : R[X] produces the polynomial with a reversed list of coefficients, equivalent to X^f.nat_degree * f(1/X).

The main result is that reverse (f * g) = reverse f * reverse g, provided the leading coefficients of f and g do not multiply to zero.

source
def polynomial.rev_at_fun (N i : ℕ) :
ℕ

If i ≤ N, then rev_at_fun N i returns N - i, otherwise it returns i. This is the map used by the embedding rev_at.

Equations
source
theorem polynomial.rev_at_fun_invol {N i : ℕ} :
polynomial.rev_at_fun N (polynomial.rev_at_fun N i) = i
source
theorem polynomial.rev_at_fun_inj {N : ℕ} :
function.injective (polynomial.rev_at_fun N)
source
def polynomial.rev_at (N : ℕ) :
ℕ ↪ ℕ

If i ≤ N, then rev_at N i returns N - i, otherwise it returns i. Essentially, this embedding is only used for i ≤ N. The advantage of rev_at N i over N - i is that rev_at is an involution.

Equations
source
@[simp]
theorem polynomial.rev_at_fun_eq (N i : ℕ) :
polynomial.rev_at_fun N i = ⇑(polynomial.rev_at N) i

We prefer to use the bundled rev_at over unbundled rev_at_fun.

source
@[simp]
theorem polynomial.rev_at_invol {N i : ℕ} :
⇑(polynomial.rev_at N) (⇑(polynomial.rev_at N) i) = i
source
@[simp]
theorem polynomial.rev_at_le {N i : ℕ} (H : i ≤ N) :
⇑(polynomial.rev_at N) i = N - i
source
theorem polynomial.rev_at_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) :
⇑(polynomial.rev_at (N + O)) (n + o) = ⇑(polynomial.rev_at N) n + ⇑(polynomial.rev_at O) o
source
@[simp]
theorem polynomial.rev_at_zero (N : ℕ) :
⇑(polynomial.rev_at N) 0 = N
source
noncomputable def polynomial.reflect {R : Type u_1} [semiring R] (N : ℕ) :
R[X] → R[X]

reflect N f is the polynomial such that (reflect N f).coeff i = f.coeff (rev_at N i). In other words, the terms with exponent [0, ..., N] now have exponent [N, ..., 0].

In practice, reflect is only used when N is at least as large as the degree of f.

Eventually, it will be used with N exactly equal to the degree of f.

Equations
source
theorem polynomial.reflect_support {R : Type u_1} [semiring R] (N : ℕ) (f : R[X]) :
(polynomial.reflect N f).support = finset.image ⇑(polynomial.rev_at N) f.support
source
@[simp]
theorem polynomial.coeff_reflect {R : Type u_1} [semiring R] (N : ℕ) (f : R[X]) (i : ℕ) :
(polynomial.reflect N f).coeff i = f.coeff (⇑(polynomial.rev_at N) i)
source
@[simp]
theorem polynomial.reflect_zero {R : Type u_1} [semiring R] {N : ℕ} :
polynomial.reflect N 0 = 0
source
@[simp]
theorem polynomial.reflect_eq_zero_iff {R : Type u_1} [semiring R] {N : ℕ} {f : R[X]} :
polynomial.reflect N f = 0 ↔ f = 0
source
@[simp]
theorem polynomial.reflect_add {R : Type u_1} [semiring R] (f g : R[X]) (N : ℕ) :
polynomial.reflect N (f + g) = polynomial.reflect N f + polynomial.reflect N g
source
@[simp]
theorem polynomial.reflect_C_mul {R : Type u_1} [semiring R] (f : R[X]) (r : R) (N : ℕ) :
polynomial.reflect N ((⇑polynomial.C r) * f) = (⇑polynomial.C r) * polynomial.reflect N f
source
@[simp]
theorem polynomial.reflect_C_mul_X_pow {R : Type u_1} [semiring R] (N n : ℕ) {c : R} :
polynomial.reflect N ((⇑polynomial.C c) * polynomial.X ^ n) = (⇑polynomial.C c) * polynomial.X ^ ⇑(polynomial.rev_at N) n
source
@[simp]
theorem polynomial.reflect_C {R : Type u_1} [semiring R] (r : R) (N : ℕ) :
polynomial.reflect N (⇑polynomial.C r) = (⇑polynomial.C r) * polynomial.X ^ N
source
@[simp]
theorem polynomial.reflect_monomial {R : Type u_1} [semiring R] (N n : ℕ) :
polynomial.reflect N (polynomial.X ^ n) = polynomial.X ^ ⇑(polynomial.rev_at N) n
source
theorem polynomial.reflect_mul_induction {R : Type u_1} [semiring R] (cf cg N O : ℕ) (f g : R[X]) :
f.support.card ≤ cf.succ → g.support.card ≤ cg.succ → f.nat_degree ≤ N → g.nat_degree ≤ O → polynomial.reflect (N + O) (f * g) = (polynomial.reflect N f) * polynomial.reflect O g
source
@[simp]
theorem polynomial.reflect_mul {R : Type u_1} [semiring R] (f g : R[X]) {F G : ℕ} (Ff : f.nat_degree ≤ F) (Gg : g.nat_degree ≤ G) :
polynomial.reflect (F + G) (f * g) = (polynomial.reflect F f) * polynomial.reflect G g
source
theorem polynomial.eval₂_reflect_mul_pow {R : Type u_1} [semiring R] {S : Type u_2} [comm_semiring S] (i : R →+* S) (x : S) [invertible x] (N : ℕ) (f : R[X]) (hf : f.nat_degree ≤ N) :
(polynomial.eval₂ i (⅟ x) (polynomial.reflect N f)) * x ^ N = polynomial.eval₂ i x f
source
theorem polynomial.eval₂_reflect_eq_zero_iff {R : Type u_1} [semiring R] {S : Type u_2} [comm_semiring S] (i : R →+* S) (x : S) [invertible x] (N : ℕ) (f : R[X]) (hf : f.nat_degree ≤ N) :
polynomial.eval₂ i (⅟ x) (polynomial.reflect N f) = 0 ↔ polynomial.eval₂ i x f = 0
source
noncomputable def polynomial.reverse {R : Type u_1} [semiring R] (f : R[X]) :
R[X]

The reverse of a polynomial f is the polynomial obtained by "reading f backwards". Even though this is not the actual definition, reverse f = f (1/X) * X ^ f.nat_degree.

Equations
source
theorem polynomial.coeff_reverse {R : Type u_1} [semiring R] (f : R[X]) (n : ℕ) :
f.reverse.coeff n = f.coeff (⇑(polynomial.rev_at f.nat_degree) n)
source
@[simp]
theorem polynomial.coeff_zero_reverse {R : Type u_1} [semiring R] (f : R[X]) :
f.reverse.coeff 0 = f.leading_coeff
source
@[simp]
theorem polynomial.reverse_zero {R : Type u_1} [semiring R] :
0.reverse = 0
source
@[simp]
theorem polynomial.reverse_eq_zero {R : Type u_1} [semiring R] {f : R[X]} :
f.reverse = 0 ↔ f = 0
source
theorem polynomial.reverse_nat_degree_le {R : Type u_1} [semiring R] (f : R[X]) :
f.reverse.nat_degree ≤ f.nat_degree
source
theorem polynomial.nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree {R : Type u_1} [semiring R] (f : R[X]) :
f.nat_degree = f.reverse.nat_degree + f.nat_trailing_degree
source
theorem polynomial.reverse_nat_degree {R : Type u_1} [semiring R] (f : R[X]) :
f.reverse.nat_degree = f.nat_degree - f.nat_trailing_degree
source
theorem polynomial.reverse_leading_coeff {R : Type u_1} [semiring R] (f : R[X]) :
f.reverse.leading_coeff = f.trailing_coeff
source
theorem polynomial.reverse_nat_trailing_degree {R : Type u_1} [semiring R] (f : R[X]) :
f.reverse.nat_trailing_degree = 0
source
theorem polynomial.reverse_trailing_coeff {R : Type u_1} [semiring R] (f : R[X]) :
f.reverse.trailing_coeff = f.leading_coeff
source
theorem polynomial.reverse_mul {R : Type u_1} [semiring R] {f g : R[X]} (fg : (f.leading_coeff) * g.leading_coeff ≠ 0) :
(f * g).reverse = (f.reverse) * g.reverse
source
@[simp]
theorem polynomial.reverse_mul_of_domain {R : Type u_1} [ring R] [no_zero_divisors R] (f g : R[X]) :
(f * g).reverse = (f.reverse) * g.reverse
source
theorem polynomial.trailing_coeff_mul {R : Type u_1} [ring R] [no_zero_divisors R] (p q : R[X]) :
(p * q).trailing_coeff = (p.trailing_coeff) * q.trailing_coeff
source
@[simp]
theorem polynomial.coeff_one_reverse {R : Type u_1} [semiring R] (f : R[X]) :
f.reverse.coeff 1 = f.next_coeff
source
theorem polynomial.eval₂_reverse_mul_pow {R : Type u_1} [semiring R] {S : Type u_2} [comm_semiring S] (i : R →+* S) (x : S) [invertible x] (f : R[X]) :
(polynomial.eval₂ i (⅟ x) f.reverse) * x ^ f.nat_degree = polynomial.eval₂ i x f
source
@[simp]
theorem polynomial.eval₂_reverse_eq_zero_iff {R : Type u_1} [semiring R] {S : Type u_2} [comm_semiring S] (i : R →+* S) (x : S) [invertible x] (f : R[X]) :
polynomial.eval₂ i (⅟ x) f.reverse = 0 ↔ polynomial.eval₂ i x f = 0
source
@[simp]
theorem polynomial.reflect_neg {R : Type u_1} [ring R] (f : R[X]) (N : ℕ) :
polynomial.reflect N (-f) = -polynomial.reflect N f
source
@[simp]
theorem polynomial.reflect_sub {R : Type u_1} [ring R] (f g : R[X]) (N : ℕ) :
polynomial.reflect N (f - g) = polynomial.reflect N f - polynomial.reflect N g
source
@[simp]
theorem polynomial.reverse_neg {R : Type u_1} [ring R] (f : R[X]) :
(-f).reverse = -f.reverse