doc-next-gen

Mathlib.Algebra.Polynomial.Eval.Degree

Module docstring

{"# Evaluation of polynomials and degrees

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

"}

Polynomial.eval₂_eq_sum_range theorem
: p.eval₂ f x = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
Full source 
theorem eval₂_eq_sum_range :
    p.eval₂ f x = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i :=
  _root_.trans (congr_arg _ p.as_sum_range)
    (_root_.trans (eval₂_finset_sum f _ _ x) (congr_arg _ (by simp)))
Polynomial Evaluation via Ring Homomorphism as Finite Sum
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $p \in R[X]$ a polynomial, and $x \in S$. Then the evaluation of $p$ at $x$ via $f$ can be expressed as: \[ \text{eval}_2(f, x, p) = \sum_{i=0}^{\deg p} f(p_i) \cdot x^i \] where $p_i$ denotes the coefficient of $X^i$ in $p$ and $\deg p$ is the natural degree of $p$.
Polynomial.eval₂_eq_sum_range' theorem
(f : R →+* S) {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) : eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i
Full source 
theorem eval₂_eq_sum_range' (f : R →+* S) {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) :
    eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i := by
  rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]
  intro i
  rw [f.map_zero, zero_mul]
Polynomial Evaluation via Ring Homomorphism as Finite Sum
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $p \in R[X]$ a polynomial, and $n \in \mathbb{N}$ such that the natural degree of $p$ satisfies $\text{natDegree}(p) < n$. Then for any $x \in S$, the evaluation of $p$ at $x$ via $f$ can be expressed as: \[ \text{eval}_2(f, x, p) = \sum_{i=0}^{n-1} f(p_i) \cdot x^i \] where $p_i$ denotes the coefficient of $X^i$ in $p$.
Polynomial.eval_eq_sum_range theorem
{p : R[X]} (x : R) : p.eval x = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i
Full source 
theorem eval_eq_sum_range {p : R[X]} (x : R) :
    p.eval x = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i := by
  rw [eval_eq_sum, sum_over_range]; simp
Polynomial Evaluation as Finite Sum Over Degree Range
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any element $x \in R$, the evaluation of $p$ at $x$ is given by the finite sum: \[ p(x) = \sum_{i=0}^{\deg p} p_i x^i \] where $p_i$ denotes the coefficient of $X^i$ in $p$ and $\deg p$ is the natural degree of $p$.
Polynomial.eval_eq_sum_range' theorem
{p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : R) : p.eval x = ∑ i ∈ Finset.range n, p.coeff i * x ^ i
Full source 
theorem eval_eq_sum_range' {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : R) :
    p.eval x = ∑ i ∈ Finset.range n, p.coeff i * x ^ i := by
  rw [eval_eq_sum, p.sum_over_range' _ _ hn]; simp
Polynomial Evaluation as Finite Sum When Degree is Bounded
Informal description
Let $p \in R[X]$ be a polynomial over a semiring $R$, and let $n \in \mathbb{N}$ be a natural number such that the natural degree of $p$ satisfies $\text{natDegree}(p) < n$. Then for any $x \in R$, the evaluation of $p$ at $x$ can be expressed as: \[ p(x) = \sum_{i=0}^{n-1} p_i x^i \] where $p_i$ denotes the coefficient of $X^i$ in $p$.
Polynomial.eval_monomial_one_add_sub theorem
[CommRing S] (d : ℕ) (y : S) : eval (1 + y) (monomial d (d + 1 : S)) - eval y (monomial d (d + 1 : S)) = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Full source 
/-- 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 eval_monomial_one_add_sub [CommRing S] (d : ℕ) (y : S) :
    eval (1 + y) (monomial d (d + 1 : S)) - eval y (monomial d (d + 1 : S)) =
      ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1)) := by
  have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]
  rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]
  simp only [one_pow, mul_one, mul_comm (y ^ _) (d.choose _)]
  rw [sum_range_succ, mul_add, Nat.choose_self, Nat.cast_one, one_mul, add_sub_cancel_right,
    mul_sum, sum_range_succ', Nat.cast_zero, zero_mul, mul_zero, add_zero]
  refine sum_congr rfl fun y _hy => ?_
  rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.succ_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]
Binomial Expansion Identity for $(1+y)^d - y^d$
Informal description
Let $S$ be a commutative ring, $d$ a natural number, and $y \in S$. Then the difference between evaluating the monomial $(d+1)X^d$ at $1+y$ and at $y$ equals the sum: \[ (d+1)(1+y)^d - (d+1)y^d = \sum_{i=0}^d \binom{d+1}{i} \cdot i \cdot y^{i-1}. \]
Polynomial.coeff_comp_degree_mul_degree theorem
(hqd0 : natDegree q ≠ 0) : coeff (p.comp q) (natDegree p * natDegree q) = leadingCoeff p * leadingCoeff q ^ natDegree p
Full source 
theorem coeff_comp_degree_mul_degree (hqd0 : natDegreenatDegree q ≠ 0) :
    coeff (p.comp q) (natDegree p * natDegree q) =
    leadingCoeff p * leadingCoeff q ^ natDegree p := by
  rw [comp, eval₂_def, coeff_sum]
  refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂
  case h₂ =>
    simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]
  case h₀ =>
    intro b hbs hbp
    refine coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)
    rw [natDegree_C, zero_add]
    refine natDegree_pow_le.trans_lt ((mul_lt_mul_right (pos_iff_ne_zero.mpr hqd0)).mpr ?_)
    exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp
  case h₁ =>
    simp +contextual
Leading Coefficient of Polynomial Composition: $\text{coeff}(p \circ q, \deg(p)\deg(q)) = \text{lc}(p) \cdot \text{lc}(q)^{\deg(p)}$
Informal description
Let $p, q \in R[X]$ be polynomials over a semiring $R$, with $q$ having a nonzero natural degree (i.e., $\text{natDegree}(q) \neq 0$). Then the coefficient of $X^{\text{natDegree}(p) \cdot \text{natDegree}(q)}$ in the composition $p \circ q$ is equal to the product of the leading coefficient of $p$ and the $\text{natDegree}(p)$-th power of the leading coefficient of $q$, i.e., \[ \text{coeff}(p \circ q, \text{natDegree}(p) \cdot \text{natDegree}(q)) = \text{lc}(p) \cdot \text{lc}(q)^{\text{natDegree}(p)}. \]
Polynomial.comp_C_mul_X_coeff theorem
{r : R} {n : ℕ} : (p.comp <| C r * X).coeff n = p.coeff n * r ^ n
Full source 
@[simp] lemma comp_C_mul_X_coeff {r : R} {n : ℕ} :
    (p.comp <| C r * X).coeff n = p.coeff n * r ^ n := by
  simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow,
    ← C_pow, finset_sum_coeff, coeff_C_mul, coeff_X_pow]
  rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]
  · intro b _ h; simp_rw [if_neg h.symm, mul_zero]
  · rw [coeff_eq_zero_of_natDegree_lt, zero_mul]
    rwa [Finset.mem_range_succ_iff, not_le] at h
Coefficient of Polynomial Composition with $rX$: $\text{coeff}(p \circ (rX), n) = p_n \cdot r^n$
Informal description
For any polynomial $p \in R[X]$, any element $r \in R$, and any natural number $n$, the coefficient of $X^n$ in the composition $p \circ (rX)$ is equal to the coefficient of $X^n$ in $p$ multiplied by $r^n$, i.e., \[ \text{coeff}(p \circ (rX), n) = \text{coeff}(p, n) \cdot r^n. \]
Polynomial.comp_C_mul_X_eq_zero_iff theorem
{r : R} (hr : r ∈ nonZeroDivisors R) : p.comp (C r * X) = 0 ↔ p = 0
Full source 
lemma comp_C_mul_X_eq_zero_iff {r : R} (hr : r ∈ nonZeroDivisors R) :
    p.comp (C r * X) = 0 ↔ p = 0 := by
  simp_rw [ext_iff]
  refine forall_congr' fun n ↦ ?_
  rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]
Composition with $rX$ is Zero iff Polynomial is Zero for Non-Zero-Divisors
Informal description
For any polynomial $p \in R[X]$ and any non-zero-divisor $r \in R$, the composition $p \circ (rX)$ is the zero polynomial if and only if $p$ is the zero polynomial. That is, \[ p \circ (rX) = 0 \leftrightarrow p = 0. \]
Polynomial.mapEquiv definition
(e : R ≃+* S) : R[X] ≃+* S[X]
Full source 
/-- If `R` and `S` are isomorphic, then so are their polynomial rings. -/
@[simps!]
def mapEquiv (e : R ≃+* S) : R[X]R[X] ≃+* S[X] :=
  RingEquiv.ofHomInv (mapRingHom (e : R →+* S)) (mapRingHom (e.symm : S →+* R)) (by ext; simp)
    (by ext; simp)
Ring isomorphism between polynomial rings induced by a ring isomorphism of coefficients
Informal description
Given a ring isomorphism \( e : R \simeq+* S \) between two semirings \( R \) and \( S \), the function `Polynomial.mapEquiv e` defines a ring isomorphism \( R[X] \simeq+* S[X] \) between their respective polynomial rings. Specifically: - The forward map applies \( e \) coefficient-wise to each polynomial in \( R[X] \). - The inverse map applies \( e^{-1} \) coefficient-wise to each polynomial in \( S[X] \). - Both maps preserve the polynomial addition and multiplication structures.
Polynomial.map_monic_eq_zero_iff theorem
(hp : p.Monic) : p.map f = 0 ↔ ∀ x, f x = 0
Full source 
theorem map_monic_eq_zero_iff (hp : p.Monic) : p.map f = 0 ↔ ∀ x, f x = 0 :=
  ⟨fun hfp x =>
    calc
      f x = f x * f p.leadingCoeff := by simp only [mul_one, hp.leadingCoeff, f.map_one]
      _ = f x * (p.map f).coeff p.natDegree := congr_arg _ (coeff_map _ _).symm
      _ = 0 := by simp only [hfp, mul_zero, coeff_zero]
      ,
    fun h => ext fun n => by simp only [h, coeff_map, coeff_zero]⟩
Monic Polynomial Maps to Zero iff Homomorphism is Trivial
Informal description
For a monic polynomial $p \in R[X]$ and a ring homomorphism $f : R \to S$, the polynomial $p$ mapped by $f$ is zero if and only if $f$ maps every element of $R$ to zero. That is, \[ f(p) = 0 \leftrightarrow \forall x \in R, f(x) = 0. \]
Polynomial.map_monic_ne_zero theorem
(hp : p.Monic) [Nontrivial S] : p.map f ≠ 0
Full source 
theorem map_monic_ne_zero (hp : p.Monic) [Nontrivial S] : p.map f ≠ 0 := fun h =>
  f.map_one_ne_zero ((map_monic_eq_zero_iff hp).mp h _)
Nonzero Image of Monic Polynomial under Ring Homomorphism with Nontrivial Codomain
Informal description
For a monic polynomial $p \in R[X]$ and a ring homomorphism $f \colon R \to S$, if the semiring $S$ is nontrivial (i.e., $0 \neq 1$ in $S$), then the polynomial obtained by applying $f$ to each coefficient of $p$ is not the zero polynomial. That is, \[ f(p) \neq 0. \]
Polynomial.degree_map_le theorem
: degree (p.map f) ≤ degree p
Full source 
lemma degree_map_le : degree (p.map f) ≤ degree p := by
  refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
  rw [degree_lt_iff_coeff_zero] at hm
  simp [hm m le_rfl]
Degree Inequality under Polynomial Map: $\deg(f(p)) \leq \deg(p)$
Informal description
For any polynomial $p \in R[X]$ and any ring homomorphism $f : R \to S$, the degree of the polynomial obtained by applying $f$ to each coefficient of $p$ is less than or equal to the degree of $p$. That is, \[ \deg(f(p)) \leq \deg(p). \]
Polynomial.natDegree_map_le theorem
: natDegree (p.map f) ≤ natDegree p
Full source 
lemma natDegree_map_le : natDegree (p.map f) ≤ natDegree p := natDegree_le_natDegree degree_map_le
Natural Degree Inequality under Polynomial Map: $\text{natDegree}(f(p)) \leq \text{natDegree}(p)$
Informal description
For any polynomial $p \in R[X]$ and any ring homomorphism $f : R \to S$, the natural degree of the polynomial obtained by applying $f$ to each coefficient of $p$ is less than or equal to the natural degree of $p$. That is, \[ \text{natDegree}(f(p)) \leq \text{natDegree}(p). \]
Polynomial.degree_map_lt theorem
(hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (p.map f).degree < p.degree
Full source 
lemma degree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (p.map f).degree < p.degree := by
  refine degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_
  rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
    at hp
  rw [← degree_eq_bot, ← hpq, hp, degree_zero]
Strict Degree Reduction under Polynomial Map with Vanishing Leading Coefficient
Informal description
Let $p \in R[X]$ be a nonzero polynomial and $f : R \to S$ be a ring homomorphism such that $f$ maps the leading coefficient of $p$ to zero. Then the degree of the polynomial obtained by applying $f$ to each coefficient of $p$ is strictly less than the degree of $p$, i.e., \[ \deg(f(p)) < \deg(p). \]
Polynomial.natDegree_map_lt theorem
(hp : f p.leadingCoeff = 0) (hp₀ : map f p ≠ 0) : (p.map f).natDegree < p.natDegree
Full source 
lemma natDegree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : mapmap f p ≠ 0) :
    (p.map f).natDegree < p.natDegree :=
  natDegree_lt_natDegree hp₀ <| degree_map_lt hp <| by rintro rfl; simp at hp₀
Natural Degree Strict Inequality under Polynomial Map with Vanishing Leading Coefficient
Informal description
Let $p \in R[X]$ be a polynomial and $f : R \to S$ be a ring homomorphism such that $f$ maps the leading coefficient of $p$ to zero. If the image of $p$ under $f$ is nonzero, then the natural degree of $f(p)$ is strictly less than the natural degree of $p$, i.e., \[ \text{natDegree}(f(p)) < \text{natDegree}(p). \]
Polynomial.natDegree_map_lt' theorem
(hp : f p.leadingCoeff = 0) (hp₀ : 0 < natDegree p) : (p.map f).natDegree < p.natDegree
Full source 
/-- Variant of `natDegree_map_lt` that assumes `0 < natDegree p` instead of `map f p ≠ 0`. -/
lemma natDegree_map_lt' (hp : f p.leadingCoeff = 0) (hp₀ : 0 < natDegree p) :
    (p.map f).natDegree < p.natDegree := by
  by_cases H : map f p = 0
  · rwa [H, natDegree_zero]
  · exact natDegree_map_lt hp H
Natural Degree Strict Inequality under Polynomial Map with Vanishing Leading Coefficient (Positive Degree Variant)
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial with positive natural degree (i.e., $0 < \text{natDegree}(p)$). If $f$ maps the leading coefficient of $p$ to zero, then the natural degree of the polynomial $f(p)$ obtained by applying $f$ to each coefficient of $p$ is strictly less than the natural degree of $p$, i.e., \[ \text{natDegree}(f(p)) < \text{natDegree}(p). \]
Polynomial.degree_map_eq_of_leadingCoeff_ne_zero theorem
(f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) : degree (p.map f) = degree p
Full source 
theorem degree_map_eq_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
    degree (p.map f) = degree p := by
  refine degree_map_le.antisymm ?_
  have hp0 : p ≠ 0 :=
    leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
  rw [degree_eq_natDegree hp0]
  refine le_degree_of_ne_zero ?_
  rw [coeff_map]
  exact hf
Degree Preservation under Polynomial Map when Leading Coefficient is Nonzero: $\deg(f(p)) = \deg(p)$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial. If the image of the leading coefficient of $p$ under $f$ is nonzero (i.e., $f(\text{leadingCoeff}(p)) \neq 0$), then the degree of the polynomial $f(p)$ obtained by applying $f$ to each coefficient of $p$ equals the degree of $p$, i.e., \[ \deg(f(p)) = \deg(p). \]
Polynomial.natDegree_map_of_leadingCoeff_ne_zero theorem
(f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) : natDegree (p.map f) = natDegree p
Full source 
theorem natDegree_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
    natDegree (p.map f) = natDegree p :=
  natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f hf)
Natural Degree Preservation under Polynomial Map when Leading Coefficient is Nonzero: $\text{natDegree}(f(p)) = \text{natDegree}(p)$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial. If the image of the leading coefficient of $p$ under $f$ is nonzero (i.e., $f(\text{leadingCoeff}(p)) \neq 0$), then the natural degree of the polynomial $f(p)$ obtained by applying $f$ to each coefficient of $p$ equals the natural degree of $p$, i.e., \[ \text{natDegree}(f(p)) = \text{natDegree}(p). \]
Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero theorem
(f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) : leadingCoeff (p.map f) = f (leadingCoeff p)
Full source 
theorem leadingCoeff_map_of_leadingCoeff_ne_zero (f : R →+* S) (hf : f (leadingCoeff p) ≠ 0) :
    leadingCoeff (p.map f) = f (leadingCoeff p) := by
  unfold leadingCoeff
  rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]
Leading Coefficient Preservation under Polynomial Map: $\text{lead}(f(p)) = f(\text{lead}(p))$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial. If the image of the leading coefficient of $p$ under $f$ is nonzero (i.e., $f(\text{leadingCoeff}(p)) \neq 0$), then the leading coefficient of the polynomial $f(p)$ obtained by applying $f$ to each coefficient of $p$ equals the image of the leading coefficient of $p$ under $f$, i.e., \[ \text{leadingCoeff}(f(p)) = f(\text{leadingCoeff}(p)). \]
Polynomial.eval₂_comp theorem
{x : S} : eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p
Full source 
theorem eval₂_comp {x : S} : eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p := by
  rw [comp, p.as_sum_range]; simp [eval₂_finset_sum, eval₂_pow]
Evaluation of Polynomial Composition via Ring Homomorphism: $\text{eval}_2(f, x, p \circ q) = \text{eval}_2(f, \text{eval}_2(f, x, q), p)$
Informal description
Let $R$ and $S$ be semirings, $f \colon R \to S$ a ring homomorphism, $p, q \in R[X]$ polynomials, and $x \in S$. Then the evaluation of the composition $p \circ q$ at $x$ via $f$ equals the evaluation of $p$ at the evaluation of $q$ at $x$ via $f$, i.e., \[ \text{eval}_2(f, x, p \circ q) = \text{eval}_2(f, \text{eval}_2(f, x, q), p). \]
Polynomial.iterate_comp_eval₂ theorem
(k : ℕ) (t : S) : eval₂ f t (p.comp^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q)
Full source 
@[simp]
theorem iterate_comp_eval₂ (k : ℕ) (t : S) :
    eval₂ f t (p.comp^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q) := by
  induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
Iterated Composition Evaluation via Ring Homomorphism: $\text{eval}_2(f, t, p \circ^k q) = (\text{eval}_2(f, \cdot, p))^k (\text{eval}_2(f, t, q))$
Informal description
Let $R$ and $S$ be semirings, $f \colon R \to S$ a ring homomorphism, $p, q \in R[X]$ polynomials, $t \in S$, and $k \in \mathbb{N}$. Then the evaluation of the $k$-th iterate of the composition operator applied to $p$ and $q$ at $t$ via $f$ equals the $k$-th iterate of the evaluation function $\lambda x. \text{eval}_2(f, x, p)$ applied to $\text{eval}_2(f, t, q)$. In other words, \[ \text{eval}_2(f, t, p \circ^k q) = (\lambda x. \text{eval}_2(f, x, p))^k (\text{eval}_2(f, t, q)). \]
Polynomial.iterate_comp_eval theorem
: ∀ (k : ℕ) (t : R), (p.comp^[k] q).eval t = (fun x => p.eval x)^[k] (q.eval t)
Full source 
@[simp]
theorem iterate_comp_eval :
    ∀ (k : ℕ) (t : R), (p.comp^[k] q).eval t = (fun x => p.eval x)^[k] (q.eval t) :=
  iterate_comp_eval₂ _
Iterated Composition Evaluation for Polynomials: $(p \circ^k q)(t) = p^k(q(t))$
Informal description
For any natural number $k$, any element $t$ in the semiring $R$, and any polynomials $p, q \in R[X]$, the evaluation of the $k$-th iterate of the composition of $p$ and $q$ at $t$ equals the $k$-th iterate of the evaluation function $\lambda x. p(x)$ applied to $q(t)$. In other words, \[ (p \circ^k q)(t) = p^k(q(t)). \]
Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map theorem
(hf : IsUnit f.leadingCoeff) (H : IsUnit (map φ f)) : IsUnit f
Full source 
lemma isUnit_of_isUnit_leadingCoeff_of_isUnit_map (hf : IsUnit f.leadingCoeff)
    (H : IsUnit (map φ f)) : IsUnit f := by
  have dz := degree_eq_zero_of_isUnit H
  rw [degree_map_eq_of_leadingCoeff_ne_zero] at dz
  · rw [eq_C_of_degree_eq_zero dz]
    refine IsUnit.map C ?_
    convert hf
    change coeff f 0 = coeff f (natDegree f)
    rw [(degree_eq_iff_natDegree_eq _).1 dz]
    · rfl
    rintro rfl
    simp at H
  · intro h
    have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf
    rw [h] at u
    simp at u
Unit Polynomial Characterization via Leading Coefficient and Map
Informal description
Let $R$ and $S$ be commutative rings, $\varphi \colon R \to S$ a ring homomorphism, and $f \in R[X]$ a polynomial. If the leading coefficient of $f$ is a unit in $R$ and the polynomial $\varphi(f)$ obtained by applying $\varphi$ to each coefficient of $f$ is a unit in $S[X]$, then $f$ itself is a unit in $R[X]$.