Documentation

Mathlib.Algebra.Polynomial.Eval.Degree

Evaluation of polynomials and degrees #

This file contains results on the interaction of Polynomial.eval and Polynomial.degree.

source
theorem Polynomial.eval₂_eq_sum_range {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
source
theorem Polynomial.eval₂_eq_sum_range' {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R →+* S) {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) :
eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
source
theorem Polynomial.eval_eq_sum_range {R : Type u} [Semiring R] {p : Polynomial R} (x : R) :
eval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i
source
theorem Polynomial.eval_eq_sum_range' {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : R) :
eval x p = ∑ i ∈ Finset.range n, p.coeff i * x ^ i
source
theorem Polynomial.eval_monomial_one_add_sub {S : Type v} [CommRing S] (d : ℕ) (y : S) :
eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) = ∑ x_1 ∈ Finset.range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

A reformulation of the expansion of (1 + y)^d: $$(d + 1) (1 + y)^d - (d + 1)y^d = \sum_{i = 0}^d {d + 1 \choose i} \cdot i \cdot y^{i - 1}.$$

source
theorem Polynomial.coeff_comp_degree_mul_degree {R : Type u} [Semiring R] {p q : Polynomial R} (hqd0 : q.natDegree ≠ 0) :
(p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
source
@[simp]
theorem Polynomial.comp_C_mul_X_coeff {R : Type u} [Semiring R] {p : Polynomial R} {r : R} {n : ℕ} :
(p.comp (C r * X)).coeff n = p.coeff n * r ^ n
source
theorem Polynomial.comp_C_mul_X_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} {r : R} (hr : r ∈ nonZeroDivisors R) :
p.comp (C r * X) = 0 ↔ p = 0
source
def Polynomial.mapEquiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) :
Polynomial R ≃+* Polynomial S

If R and S are isomorphic, then so are their polynomial rings.

Equations
Instances For
    source
    @[simp]
    theorem Polynomial.mapEquiv_symm_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial S) :
    (mapEquiv e).symm a = map (↑e.symm) a
    source
    @[simp]
    theorem Polynomial.mapEquiv_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial R) :
    (mapEquiv e) a = map (↑e) a
    source
    theorem Polynomial.map_monic_eq_zero_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : p.Monic) :
    map f p = 0 ↔ ∀ (x : R), f x = 0
    source
    theorem Polynomial.map_monic_ne_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : p.Monic) [Nontrivial S] :
    map f p ≠ 0
    source
    theorem Polynomial.degree_map_le {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
    (map f p).degree ≤ p.degree
    source
    theorem Polynomial.natDegree_map_le {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
    (map f p).natDegree ≤ p.natDegree
    source
    theorem Polynomial.degree_map_lt {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) :
    (map f p).degree < p.degree
    source
    theorem Polynomial.natDegree_map_lt {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : map f p ≠ 0) :
    (map f p).natDegree < p.natDegree
    source
    theorem Polynomial.natDegree_map_lt' {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} (hp : f p.leadingCoeff = 0) (hp₀ : 0 < p.natDegree) :
    (map f p).natDegree < p.natDegree

    Variant of natDegree_map_lt that assumes 0 < natDegree p instead of map f p ≠ 0.

    source
    theorem Polynomial.degree_map_eq_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) :
    (map f p).degree = p.degree
    source
    theorem Polynomial.natDegree_map_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) :
    (map f p).natDegree = p.natDegree
    source
    theorem Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero {R : Type u} {S : Type v} [Semiring R] [Semiring S] {p : Polynomial R} (f : R →+* S) (hf : f p.leadingCoeff ≠ 0) :
    (map f p).leadingCoeff = f p.leadingCoeff
    source
    theorem Polynomial.eval₂_comp {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) {x : S} :
    eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p
    source
    @[simp]
    theorem Polynomial.iterate_comp_eval₂ {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) (k : ℕ) (t : S) :
    eval₂ f t (p.comp^[k] q) = (fun (x : S) => eval₂ f x p)^[k] (eval₂ f t q)
    source
    @[simp]
    theorem Polynomial.iterate_comp_eval {R : Type u} [CommSemiring R] {p q : Polynomial R} (k : ℕ) (t : R) :
    eval t (p.comp^[k] q) = (fun (x : R) => eval x p)^[k] (eval t q)
    source
    theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map {R : Type u} {S : Type v} [Semiring R] [CommRing S] [IsDomain S] (φ : R →+* S) {f : Polynomial R} (hf : IsUnit f.leadingCoeff) (H : IsUnit (map φ f)) :
    IsUnit f