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) : eval₂ f x p = ∑ i ∈ Finset.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) : eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i

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

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

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}.$$

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

@[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

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

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

• Polynomial.mapEquiv e = RingEquiv.ofHomInv (Polynomial.mapRingHom ↑e) (Polynomial.mapRingHom ↑e.symm) ⋯ ⋯

@[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

@[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

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

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

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

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

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

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

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.

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

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

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

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

@[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)

@[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)

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