HepLean Documentation

Mathlib.Algebra.Polynomial.Eval.Degree

Evaluation of polynomials and degrees #

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

theorem Polynomial.eval₂_eq_sum_range {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (x : S) :
Polynomial.eval₂ f x p = iFinset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
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) :
Polynomial.eval₂ f x p = iFinset.range n, f (p.coeff i) * x ^ i
theorem Polynomial.eval_eq_sum_range {R : Type u} [Semiring R] {p : Polynomial R} (x : R) :
Polynomial.eval x p = iFinset.range (p.natDegree + 1), p.coeff i * x ^ i
theorem Polynomial.eval_eq_sum_range' {R : Type u} [Semiring R] {p : Polynomial R} {n : } (hn : p.natDegree < n) (x : R) :
Polynomial.eval x p = iFinset.range n, p.coeff i * x ^ i
theorem Polynomial.eval_monomial_one_add_sub {S : Type v} [CommRing S] (d : ) (y : S) :
Polynomial.eval (1 + y) ((Polynomial.monomial d) (d + 1)) - Polynomial.eval y ((Polynomial.monomial d) (d + 1)) = x_1Finset.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}.$$

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
def Polynomial.mapEquiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) :

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

Equations
Instances For
    @[simp]
    theorem Polynomial.mapEquiv_symm_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial S) :
    (Polynomial.mapEquiv e).symm a = Polynomial.map (↑e.symm) a
    @[simp]
    theorem Polynomial.mapEquiv_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (e : R ≃+* S) (a : Polynomial R) :
    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) :
    Polynomial.map f p = 0 ∀ (x : R), f x = 0
    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] :
    theorem Polynomial.degree_map_le {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
    (Polynomial.map f p).degree p.degree
    theorem Polynomial.natDegree_map_le {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} {p : Polynomial R} :
    (Polynomial.map f p).natDegree p.natDegree
    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) :
    (Polynomial.map f p).degree < p.degree
    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₀ : Polynomial.map f p 0) :
    (Polynomial.map f p).natDegree < p.natDegree
    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) :
    (Polynomial.map f p).natDegree < p.natDegree

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

    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) :
    (Polynomial.map f p).degree = p.degree
    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) :
    (Polynomial.map f p).natDegree = p.natDegree
    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) :
    (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
    theorem Polynomial.eval₂_comp {R : Type u} {S : Type v} [Semiring R] {p q : Polynomial R} [CommSemiring S] (f : R →+* S) {x : S} :
    @[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) :
    Polynomial.eval₂ f t (p.comp^[k] q) = (fun (x : S) => Polynomial.eval₂ f x p)^[k] (Polynomial.eval₂ f t q)
    @[simp]
    theorem Polynomial.iterate_comp_eval {R : Type u} [CommSemiring R] {p q : Polynomial R} (k : ) (t : R) :
    Polynomial.eval t (p.comp^[k] q) = (fun (x : R) => Polynomial.eval x p)^[k] (Polynomial.eval t q)
    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 (Polynomial.map φ f)) :