doc-next-gen

Mathlib.Algebra.Polynomial.Eval.Defs

Module docstring

{"# Evaluating a polynomial

Main definitions

  • Polynomial.eval₂: evaluate p : R[X] in S given a ring hom f : R →+* S and x : S.
  • Polynomial.eval: evaluate p : R[X] given x : R.
  • Polynomial.IsRoot: x : R is a root of p : R[X].
  • Polynomial.comp: compose two polynomials p q : R[X] by evaluating p at q.
  • Polynomial.map: apply f : R →+* S to the coefficients of p : R[X].

We also provide the following bundled versions: * Polynomial.eval₂AddMonoidHom, Polynomial.eval₂RingHom * Polynomial.evalRingHom * Polynomial.compRingHom * Polynomial.mapRingHom

We include results on applying the definitions to C, X and ring operations.

","We next prove that eval₂ is multiplicative as long as target ring is commutative (even if the source ring is not). "}

Polynomial.eval₂ definition
Full source 
/-- Evaluate a polynomial `p` given a ring hom `f` from the scalar ring
  to the target and a value `x` for the variable in the target -/
irreducible_def eval₂ (p : R[X]) : S :=
  p.sum fun e a => f a * x ^ e
Evaluation of a polynomial via a ring homomorphism
Informal description
Given a polynomial $p \in R[X]$, a ring homomorphism $f: R \to S$, and an element $x \in S$, the evaluation of $p$ at $x$ via $f$ is defined as the sum $\sum_{e} f(a_e) \cdot x^e$, where $a_e$ are the coefficients of $p$.
Polynomial.eval₂_def theorem
: eta_helper Eq✝ @eval₂.{} @(delta% @definition✝)
Full source 
/-- Evaluate a polynomial `p` given a ring hom `f` from the scalar ring
  to the target and a value `x` for the variable in the target -/
irreducible_def eval₂ (p : R[X]) : S :=
  p.sum fun e a => f a * x ^ e
Definition of Polynomial Evaluation via Ring Homomorphism
Informal description
The evaluation of a polynomial $p \in R[X]$ via a ring homomorphism $f: R \to S$ at an element $x \in S$ is defined as the sum $\sum_{e} f(a_e) \cdot x^e$, where $a_e$ are the coefficients of $p$.
Polynomial.eval₂_eq_sum theorem
{f : R →+* S} {x : S} : p.eval₂ f x = p.sum fun e a => f a * x ^ e
Full source 
theorem eval₂_eq_sum {f : R →+* S} {x : S} : p.eval₂ f x = p.sum fun e a => f a * x ^ e := by
  rw [eval₂_def]
Polynomial Evaluation as Sum of Scaled Powers: $\text{eval}_2(f, x, p) = \sum_e f(a_e) x^e$
Informal description
For any polynomial $p \in R[X]$, ring homomorphism $f: R \to S$, and element $x \in S$, the evaluation of $p$ at $x$ via $f$ equals the sum $\sum_{e} f(a_e) \cdot x^e$, where $a_e$ are the coefficients of $p$.
Polynomial.eval₂_congr theorem
{R S : Type*} [Semiring R] [Semiring S] {f g : R →+* S} {s t : S} {φ ψ : R[X]} : f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ
Full source 
theorem eval₂_congr {R S : Type*} [Semiring R] [Semiring S] {f g : R →+* S} {s t : S}
    {φ ψ : R[X]} : f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ := by
  rintro rfl rfl rfl; rfl
Congruence of Polynomial Evaluation via Ring Homomorphisms
Informal description
Let $R$ and $S$ be semirings, $f, g: R \to S$ be ring homomorphisms, $s, t \in S$, and $\varphi, \psi \in R[X]$ be polynomials. If $f = g$, $s = t$, and $\varphi = \psi$, then the evaluations $\varphi$ at $s$ via $f$ and $\psi$ at $t$ via $g$ are equal, i.e., $\text{eval}_2(f, s, \varphi) = \text{eval}_2(g, t, \psi)$.
Polynomial.eval₂_zero theorem
: (0 : R[X]).eval₂ f x = 0
Full source 
@[simp]
theorem eval₂_zero : (0 : R[X]).eval₂ f x = 0 := by simp [eval₂_eq_sum]
Evaluation of Zero Polynomial Yields Zero
Informal description
For any semiring $R$, any ring homomorphism $f : R \to S$, and any element $x \in S$, the evaluation of the zero polynomial $0 \in R[X]$ at $x$ via $f$ is equal to the zero element of $S$, i.e., $\text{eval}_2(f, x, 0) = 0_S$.
Polynomial.eval₂_C theorem
: (C a).eval₂ f x = f a
Full source 
@[simp]
theorem eval₂_C : (C a).eval₂ f x = f a := by simp [eval₂_eq_sum]
Evaluation of Constant Polynomial via Ring Homomorphism: $\text{eval}_2(f, x, C(a)) = f(a)$
Informal description
For any semiring $R$, any ring homomorphism $f \colon R \to S$, any element $a \in R$, and any element $x \in S$, the evaluation of the constant polynomial $C(a)$ at $x$ via $f$ equals $f(a)$, i.e., \[ \text{eval}_2(f, x, C(a)) = f(a). \]
Polynomial.eval₂_X theorem
: X.eval₂ f x = x
Full source 
@[simp]
theorem eval₂_X : X.eval₂ f x = x := by simp [eval₂_eq_sum]
Evaluation of $X$ via ring homomorphism: $\text{eval}_2(f, x, X) = x$
Informal description
For any ring homomorphism $f \colon R \to S$ and any element $x \in S$, the evaluation of the polynomial $X \in R[X]$ at $x$ via $f$ equals $x$, i.e., $\text{eval}_2(f, x, X) = x$.
Polynomial.eval₂_monomial theorem
{n : ℕ} {r : R} : (monomial n r).eval₂ f x = f r * x ^ n
Full source 
@[simp]
theorem eval₂_monomial {n : ℕ} {r : R} : (monomial n r).eval₂ f x = f r * x ^ n := by
  simp [eval₂_eq_sum]
Evaluation of Monomial via Ring Homomorphism: $\text{eval}_2(f, x, rX^n) = f(r) x^n$
Informal description
For any natural number $n$, element $r \in R$, ring homomorphism $f \colon R \to S$, and element $x \in S$, the evaluation of the monomial $rX^n$ at $x$ via $f$ is given by $f(r) \cdot x^n$.
Polynomial.eval₂_X_pow theorem
{n : ℕ} : (X ^ n).eval₂ f x = x ^ n
Full source 
@[simp]
theorem eval₂_X_pow {n : ℕ} : (X ^ n).eval₂ f x = x ^ n := by
  rw [X_pow_eq_monomial]
  convert eval₂_monomial f x (n := n) (r := 1)
  simp
Evaluation of $X^n$ via Ring Homomorphism: $\text{eval}_2(f, x, X^n) = x^n$
Informal description
For any natural number $n$, ring homomorphism $f \colon R \to S$, and element $x \in S$, the evaluation of the polynomial $X^n \in R[X]$ at $x$ via $f$ is equal to $x^n$, i.e., $\text{eval}_2(f, x, X^n) = x^n$.
Polynomial.eval₂_add theorem
: (p + q).eval₂ f x = p.eval₂ f x + q.eval₂ f x
Full source 
@[simp]
theorem eval₂_add : (p + q).eval₂ f x = p.eval₂ f x + q.eval₂ f x := by
  simp only [eval₂_eq_sum]
  apply sum_add_index <;> simp [add_mul]
Additivity of Polynomial Evaluation via Ring Homomorphism: $\text{eval}_2(f, x, p + q) = \text{eval}_2(f, x, p) + \text{eval}_2(f, x, q)$
Informal description
For any polynomials $p, q \in R[X]$, ring homomorphism $f : R \to S$, and element $x \in S$, the evaluation of the sum $p + q$ at $x$ via $f$ equals the sum of the evaluations of $p$ and $q$ at $x$ via $f$. That is, \[ \text{eval}_2(f, x, p + q) = \text{eval}_2(f, x, p) + \text{eval}_2(f, x, q). \]
Polynomial.eval₂_one theorem
: (1 : R[X]).eval₂ f x = 1
Full source 
@[simp]
theorem eval₂_one : (1 : R[X]).eval₂ f x = 1 := by rw [← C_1, eval₂_C, f.map_one]
Evaluation of the Constant Polynomial One via Ring Homomorphism: $\text{eval}_2(f, x, 1) = 1$
Informal description
For any ring homomorphism $f \colon R \to S$ and any element $x \in S$, the evaluation of the constant polynomial $1 \in R[X]$ at $x$ via $f$ equals the multiplicative identity $1 \in S$, i.e., \[ \text{eval}_2(f, x, 1) = 1. \]
Polynomial.eval₂AddMonoidHom definition
: R[X] →+ S
Full source 
/-- `eval₂AddMonoidHom (f : R →+* S) (x : S)` is the `AddMonoidHom` from
`R[X]` to `S` obtained by evaluating the pushforward of `p` along `f` at `x`. -/
@[simps]
def eval₂AddMonoidHom : R[X]R[X] →+ S where
  toFun := eval₂ f x
  map_zero' := eval₂_zero _ _
  map_add' _ _ := eval₂_add _ _
Additive monoid homomorphism for polynomial evaluation via ring homomorphism
Informal description
Given a ring homomorphism \( f : R \to S \) and an element \( x \in S \), the function \( \text{eval}_2(f, x) : R[X] \to S \) is an additive monoid homomorphism that evaluates a polynomial \( p \in R[X] \) at \( x \) via \( f \). Specifically, it satisfies: 1. \( \text{eval}_2(f, x)(0) = 0 \) 2. \( \text{eval}_2(f, x)(p + q) = \text{eval}_2(f, x)(p) + \text{eval}_2(f, x)(q) \) for any \( p, q \in R[X] \)
Polynomial.eval₂_natCast theorem
(n : ℕ) : (n : R[X]).eval₂ f x = n
Full source 
@[simp]
theorem eval₂_natCast (n : ℕ) : (n : R[X]).eval₂ f x = n := by
  induction n with
  | zero => simp only [eval₂_zero, Nat.cast_zero]
  | succ n ih => rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
Evaluation of Constant Polynomial via Ring Homomorphism: $\text{eval}_2(f, x, n) = n$
Informal description
For any natural number $n$, ring homomorphism $f \colon R \to S$, and element $x \in S$, the evaluation of the constant polynomial $n \in R[X]$ at $x$ via $f$ equals $n$ itself, i.e., \[ \text{eval}_2(f, x, n) = n. \]
Polynomial.eval₂_ofNat theorem
{S : Type*} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) : (ofNat(n) : R[X]).eval₂ f a = ofNat(n)
Full source 
@[simp]
lemma eval₂_ofNat {S : Type*} [Semiring S] (n : ℕ) [n.AtLeastTwo] (f : R →+* S) (a : S) :
    (ofNat(n) : R[X]).eval₂ f a = ofNat(n) := by
  simp [OfNat.ofNat]
Evaluation of Constant Polynomial via Ring Homomorphism: $\text{eval}_2(f, a, n) = n$ for $n \geq 2$
Informal description
Let $R$ and $S$ be semirings, $f \colon R \to S$ a ring homomorphism, and $a \in S$. For any natural number $n \geq 2$, the evaluation of the constant polynomial $n \in R[X]$ at $a$ via $f$ equals $n$ itself, i.e., \[ \text{eval}_2(f, a, n) = n. \]
Polynomial.eval₂_sum theorem
(p : T[X]) (g : ℕ → T → R[X]) (x : S) : (p.sum g).eval₂ f x = p.sum fun n a => (g n a).eval₂ f x
Full source 
theorem eval₂_sum (p : T[X]) (g : ℕ → T → R[X]) (x : S) :
    (p.sum g).eval₂ f x = p.sum fun n a => (g n a).eval₂ f x := by
  let T : R[X]R[X] →+ S :=
    { toFun := eval₂ f x
      map_zero' := eval₂_zero _ _
      map_add' := fun p q => eval₂_add _ _ }
  have A : ∀ y, eval₂ f x y = T y := fun y => rfl
  simp only [A]
  rw [sum, map_sum, sum]
Linearity of Polynomial Evaluation via Ring Homomorphism over Sums
Informal description
Let $R$, $S$, and $T$ be semirings, $f : R \to S$ be a ring homomorphism, $x \in S$, and $p \in T[X]$. For any function $g : \mathbb{N} \to T \to R[X]$, the evaluation of the sum polynomial $\sum_{n} g(n, a_n)$ at $x$ via $f$ equals the sum of the evaluations of each $g(n, a_n)$ at $x$ via $f$. That is, \[ \text{eval}_2(f, x, \sum_{n} g(n, a_n)) = \sum_{n} \text{eval}_2(f, x, g(n, a_n)). \]
Polynomial.eval₂_list_sum theorem
(l : List R[X]) (x : S) : eval₂ f x l.sum = (l.map (eval₂ f x)).sum
Full source 
theorem eval₂_list_sum (l : List R[X]) (x : S) : eval₂ f x l.sum = (l.map (eval₂ f x)).sum :=
  map_list_sum (eval₂AddMonoidHom f x) l
Evaluation of Polynomial Sum over a List via Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ be a ring homomorphism, and $x \in S$. For any list of polynomials $l$ in $R[X]$, the evaluation of the sum of polynomials in $l$ at $x$ via $f$ equals the sum of the evaluations of each polynomial in $l$ at $x$ via $f$. That is, \[ \text{eval}_2(f, x, \sum_{p \in l} p) = \sum_{p \in l} \text{eval}_2(f, x, p). \]
Polynomial.eval₂_multiset_sum theorem
(s : Multiset R[X]) (x : S) : eval₂ f x s.sum = (s.map (eval₂ f x)).sum
Full source 
theorem eval₂_multiset_sum (s : Multiset R[X]) (x : S) :
    eval₂ f x s.sum = (s.map (eval₂ f x)).sum :=
  map_multiset_sum (eval₂AddMonoidHom f x) s
Evaluation of Polynomial Sum via Ring Homomorphism Equals Sum of Evaluations
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $x \in S$. For any multiset $s$ of polynomials in $R[X]$, the evaluation of the sum of polynomials in $s$ at $x$ via $f$ equals the sum of the evaluations of each polynomial in $s$ at $x$ via $f$. That is, \[ \text{eval}_2(f, x, \sum_{p \in s} p) = \sum_{p \in s} \text{eval}_2(f, x, p). \]
Polynomial.eval₂_finset_sum theorem
(s : Finset ι) (g : ι → R[X]) (x : S) : (∑ i ∈ s, g i).eval₂ f x = ∑ i ∈ s, (g i).eval₂ f x
Full source 
theorem eval₂_finset_sum (s : Finset ι) (g : ι → R[X]) (x : S) :
    (∑ i ∈ s, g i).eval₂ f x = ∑ i ∈ s, (g i).eval₂ f x :=
  map_sum (eval₂AddMonoidHom f x) _ _
Linearity of Polynomial Evaluation over Finite Sums
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $s$ a finite set of indices. For any family of polynomials $(g_i)_{i \in s}$ in $R[X]$, the evaluation of the sum $\sum_{i \in s} g_i$ at $x$ via $f$ equals the sum of the evaluations of each $g_i$ at $x$ via $f$. That is, $$\left(\sum_{i \in s} g_i\right).\text{eval}_2(f, x) = \sum_{i \in s} (g_i.\text{eval}_2(f, x))$$
Polynomial.eval₂_ofFinsupp theorem
{f : R →+* S} {x : S} {p : R[ℕ]} : eval₂ f x (⟨p⟩ : R[X]) = liftNC (↑f) (powersHom S x) p
Full source 
theorem eval₂_ofFinsupp {f : R →+* S} {x : S} {p : R[ℕ]} :
    eval₂ f x (⟨p⟩ : R[X]) = liftNC (↑f) (powersHom S x) p := by
  simp only [eval₂_eq_sum, sum, toFinsupp_sum, support, coeff]
  rfl
Evaluation of Polynomial via Ring Homomorphism Equals Non-Commutative Lift of Powers Homomorphism
Informal description
Let $R$ and $S$ be semirings, $f: R \to S$ a ring homomorphism, $x \in S$, and $p$ a polynomial in $R[X]$ represented as a finitely supported function $p: \mathbb{N} \to R$. Then the evaluation of $p$ at $x$ via $f$ equals the non-commutative lift of $f$ and the powers homomorphism evaluated at $x$, applied to $p$. That is, $$\text{eval}_2(f, x, \langle p \rangle) = \text{liftNC}(f, \text{powersHom}_S(x))(p)$$ where: - $\langle p \rangle$ denotes the polynomial representation of $p$ - $\text{powersHom}_S(x)$ is the monoid homomorphism sending $n$ to $x^n$ - $\text{liftNC}$ is the non-commutative lift operation for the additive monoid algebra
Polynomial.eval₂_mul_noncomm theorem
(hf : ∀ k, Commute (f <| q.coeff k) x) : eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q
Full source 
theorem eval₂_mul_noncomm (hf : ∀ k, Commute (f <| q.coeff k) x) :
    eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q := by
  rcases p with ⟨p⟩; rcases q with ⟨q⟩
  simp only [coeff] at hf
  simp only [← ofFinsupp_mul, eval₂_ofFinsupp]
  exact liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n
Multiplicativity of Polynomial Evaluation under Commutation Condition
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $p, q \in R[X]$ polynomials. If for every natural number $k$, the element $f(q_k)$ commutes with $x$ in $S$ (where $q_k$ is the coefficient of $X^k$ in $q$), then the evaluation of the product $p \cdot q$ at $x$ via $f$ equals the product of the evaluations of $p$ and $q$ at $x$ via $f$. That is, $$\text{eval}_2(f, x, p \cdot q) = \text{eval}_2(f, x, p) \cdot \text{eval}_2(f, x, q).$$
Polynomial.eval₂_mul_X theorem
: eval₂ f x (p * X) = eval₂ f x p * x
Full source 
@[simp]
theorem eval₂_mul_X : eval₂ f x (p * X) = eval₂ f x p * x := by
  refine _root_.trans (eval₂_mul_noncomm _ _ fun k => ?_) (by rw [eval₂_X])
  rcases em (k = 1) with (rfl | hk)
  · simp
  · simp [coeff_X_of_ne_one hk]
Evaluation of $p \cdot X$: $\text{eval}_2(f, x, p \cdot X) = \text{eval}_2(f, x, p) \cdot x$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $p \in R[X]$ a polynomial. Then the evaluation of the product $p \cdot X$ at $x$ via $f$ equals the evaluation of $p$ at $x$ via $f$ multiplied by $x$, i.e., $$\text{eval}_2(f, x, p \cdot X) = \text{eval}_2(f, x, p) \cdot x.$$
Polynomial.eval₂_X_mul theorem
: eval₂ f x (X * p) = eval₂ f x p * x
Full source 
@[simp]
theorem eval₂_X_mul : eval₂ f x (X * p) = eval₂ f x p * x := by rw [X_mul, eval₂_mul_X]
Evaluation of $X \cdot p$: $\text{eval}_2(f, x, X \cdot p) = \text{eval}_2(f, x, p) \cdot x$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $p \in R[X]$ a polynomial. Then the evaluation of the product $X \cdot p$ at $x$ via $f$ equals the evaluation of $p$ at $x$ via $f$ multiplied by $x$, i.e., $$\text{eval}_2(f, x, X \cdot p) = \text{eval}_2(f, x, p) \cdot x.$$
Polynomial.eval₂_mul_C' theorem
(h : Commute (f a) x) : eval₂ f x (p * C a) = eval₂ f x p * f a
Full source 
theorem eval₂_mul_C' (h : Commute (f a) x) : eval₂ f x (p * C a) = eval₂ f x p * f a := by
  rw [eval₂_mul_noncomm, eval₂_C]
  intro k
  by_cases hk : k = 0
  · simp only [hk, h, coeff_C_zero, coeff_C_ne_zero]
  · simp only [coeff_C_ne_zero hk, RingHom.map_zero, Commute.zero_left]
Evaluation of Polynomial Multiplied by Constant: $\text{eval}_2(f, x, p \cdot C(a)) = \text{eval}_2(f, x, p) \cdot f(a)$ under Commutation Condition
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $p \in R[X]$ a polynomial. If $f(a)$ commutes with $x$ in $S$ for some $a \in R$, then the evaluation of the product $p \cdot C(a)$ at $x$ via $f$ equals the product of the evaluation of $p$ at $x$ via $f$ and $f(a)$. That is, $$\text{eval}_2(f, x, p \cdot C(a)) = \text{eval}_2(f, x, p) \cdot f(a).$$
Polynomial.eval₂_list_prod_noncomm theorem
(ps : List R[X]) (hf : ∀ p ∈ ps, ∀ (k), Commute (f <| coeff p k) x) : eval₂ f x ps.prod = (ps.map (Polynomial.eval₂ f x)).prod
Full source 
theorem eval₂_list_prod_noncomm (ps : List R[X])
    (hf : ∀ p ∈ ps, ∀ (k), Commute (f <| coeff p k) x) :
    eval₂ f x ps.prod = (ps.map (Polynomial.eval₂ f x)).prod := by
  induction' ps using List.reverseRecOn with ps p ihp
  · simp
  · simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
    simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]
Multiplicativity of Polynomial List Product Evaluation under Commutation Condition
Informal description
Let $R$ and $S$ be semirings, $f \colon R \to S$ a ring homomorphism, $x \in S$, and $ps$ a list of polynomials in $R[X]$. If for every polynomial $p$ in $ps$ and every natural number $k$, the element $f(p_k)$ commutes with $x$ (where $p_k$ is the coefficient of $X^k$ in $p$), then the evaluation of the product of polynomials in $ps$ at $x$ via $f$ equals the product of the evaluations of each polynomial in $ps$ at $x$ via $f$. That is, $$\text{eval}_2(f, x, \prod_{p \in ps} p) = \prod_{p \in ps} \text{eval}_2(f, x, p).$$
Polynomial.eval₂RingHom' definition
(f : R →+* S) (x : S) (hf : ∀ a, Commute (f a) x) : R[X] →+* S
Full source 
/-- `eval₂` as a `RingHom` for noncommutative rings -/
@[simps]
def eval₂RingHom' (f : R →+* S) (x : S) (hf : ∀ a, Commute (f a) x) : R[X]R[X] →+* S where
  toFun := eval₂ f x
  map_add' _ _ := eval₂_add _ _
  map_zero' := eval₂_zero _ _
  map_mul' _p q := eval₂_mul_noncomm f x fun k => hf <| coeff q k
  map_one' := eval₂_one _ _
Ring homomorphism induced by polynomial evaluation via \( f \) and \( x \)
Informal description
Given a ring homomorphism \( f : R \to S \), an element \( x \in S \), and the condition that \( f(a) \) commutes with \( x \) for all \( a \in R \), the function \( \text{eval}_2(f, x) \) is a ring homomorphism from \( R[X] \) to \( S \). This means it preserves addition, multiplication, zero, and one: - \( \text{eval}_2(f, x, p + q) = \text{eval}_2(f, x, p) + \text{eval}_2(f, x, q) \) - \( \text{eval}_2(f, x, p \cdot q) = \text{eval}_2(f, x, p) \cdot \text{eval}_2(f, x, q) \) - \( \text{eval}_2(f, x, 0) = 0 \) - \( \text{eval}_2(f, x, 1) = 1 \).
Polynomial.eval₂_mul theorem
: (p * q).eval₂ f x = p.eval₂ f x * q.eval₂ f x
Full source 
@[simp]
theorem eval₂_mul : (p * q).eval₂ f x = p.eval₂ f x * q.eval₂ f x :=
  eval₂_mul_noncomm _ _ fun _k => Commute.all _ _
Multiplicativity of Polynomial Evaluation under Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $p, q \in R[X]$ polynomials. Then the evaluation of the product $p \cdot q$ at $x$ via $f$ equals the product of the evaluations of $p$ and $q$ at $x$ via $f$. That is, $$\text{eval}_2(f, x, p \cdot q) = \text{eval}_2(f, x, p) \cdot \text{eval}_2(f, x, q).$$
Polynomial.eval₂_mul_eq_zero_of_left theorem
(q : R[X]) (hp : p.eval₂ f x = 0) : (p * q).eval₂ f x = 0
Full source 
theorem eval₂_mul_eq_zero_of_left (q : R[X]) (hp : p.eval₂ f x = 0) : (p * q).eval₂ f x = 0 := by
  rw [eval₂_mul f x]
  exact mul_eq_zero_of_left hp (q.eval₂ f x)
Vanishing of Polynomial Product Evaluation When Left Factor Vanishes
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $p, q \in R[X]$ polynomials. If the evaluation of $p$ at $x$ via $f$ is zero, then the evaluation of the product $p \cdot q$ at $x$ via $f$ is also zero. That is, if $\text{eval}_2(f, x, p) = 0$, then $\text{eval}_2(f, x, p \cdot q) = 0$.
Polynomial.eval₂_mul_eq_zero_of_right theorem
(p : R[X]) (hq : q.eval₂ f x = 0) : (p * q).eval₂ f x = 0
Full source 
theorem eval₂_mul_eq_zero_of_right (p : R[X]) (hq : q.eval₂ f x = 0) : (p * q).eval₂ f x = 0 := by
  rw [eval₂_mul f x]
  exact mul_eq_zero_of_right (p.eval₂ f x) hq
Vanishing of Polynomial Product Evaluation When Right Factor Vanishes
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $x \in S$, and $p, q \in R[X]$ polynomials. If the evaluation of $q$ at $x$ via $f$ is zero, then the evaluation of the product $p \cdot q$ at $x$ via $f$ is also zero. That is, if $\text{eval}_2(f, x, q) = 0$, then $\text{eval}_2(f, x, p \cdot q) = 0$.
Polynomial.eval₂RingHom definition
(f : R →+* S) (x : S) : R[X] →+* S
Full source 
/-- `eval₂` as a `RingHom` -/
def eval₂RingHom (f : R →+* S) (x : S) : R[X]R[X] →+* S :=
  { eval₂AddMonoidHom f x with
    map_one' := eval₂_one _ _
    map_mul' := fun _ _ => eval₂_mul _ _ }
Semiring homomorphism for polynomial evaluation via ring homomorphism
Informal description
Given a semiring homomorphism \( f : R \to S \) and an element \( x \in S \), the function \( \text{eval}_2(f, x) : R[X] \to S \) is a semiring homomorphism that evaluates a polynomial \( p \in R[X] \) at \( x \) via \( f \). Specifically, it satisfies: 1. \( \text{eval}_2(f, x)(1) = 1 \) 2. \( \text{eval}_2(f, x)(p \cdot q) = \text{eval}_2(f, x)(p) \cdot \text{eval}_2(f, x)(q) \) for any \( p, q \in R[X] \) 3. \( \text{eval}_2(f, x)(p + q) = \text{eval}_2(f, x)(p) + \text{eval}_2(f, x)(q) \) for any \( p, q \in R[X] \) 4. \( \text{eval}_2(f, x)(0) = 0 \)
Polynomial.coe_eval₂RingHom theorem
(f : R →+* S) (x) : ⇑(eval₂RingHom f x) = eval₂ f x
Full source 
@[simp]
theorem coe_eval₂RingHom (f : R →+* S) (x) : ⇑(eval₂RingHom f x) = eval₂ f x :=
  rfl
Coincidence of Evaluation Homomorphism and Evaluation Function
Informal description
For any semiring homomorphism $f \colon R \to S$ and any element $x \in S$, the underlying function of the evaluation homomorphism $\text{eval}_2(f, x) \colon R[X] \to S$ coincides with the polynomial evaluation function $\text{eval}_2(f, x)$.
Polynomial.eval₂_pow theorem
(n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n
Full source 
theorem eval₂_pow (n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n :=
  (eval₂RingHom _ _).map_pow _ _
Power Law for Polynomial Evaluation via Ring Homomorphism: $(p^n).\text{eval}_2(f, x) = (p.\text{eval}_2(f, x))^n$
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$. For any natural number $n$, the evaluation of $p^n$ at $x$ via $f$ equals the $n$-th power of the evaluation of $p$ at $x$ via $f$, i.e., $$(p^n).\text{eval}_2(f, x) = (p.\text{eval}_2(f, x))^n.$$
Polynomial.eval₂_dvd theorem
: p ∣ q → eval₂ f x p ∣ eval₂ f x q
Full source 
theorem eval₂_dvd : p ∣ q → eval₂eval₂ f x p ∣ eval₂ f x q :=
  (eval₂RingHom f x).map_dvd
Divisibility Preservation Under Polynomial Evaluation via Ring Homomorphism
Informal description
Let $R$ be a semiring, $S$ a commutative semiring, $f : R \to S$ a ring homomorphism, and $x \in S$. For any polynomials $p, q \in R[X]$, if $p$ divides $q$ in $R[X]$, then the evaluation of $p$ at $x$ via $f$ divides the evaluation of $q$ at $x$ via $f$ in $S$.
Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero theorem
(h : p ∣ q) (h0 : eval₂ f x p = 0) : eval₂ f x q = 0
Full source 
theorem eval₂_eq_zero_of_dvd_of_eval₂_eq_zero (h : p ∣ q) (h0 : eval₂ f x p = 0) :
    eval₂ f x q = 0 :=
  zero_dvd_iff.mp (h0 ▸ eval₂_dvd f x h)
Zero Preservation Under Divisibility in Polynomial Evaluation via Ring Homomorphism
Informal description
Let $R$ be a semiring, $S$ a commutative semiring, $f \colon R \to S$ a ring homomorphism, and $x \in S$. For any polynomials $p, q \in R[X]$, if $p$ divides $q$ and the evaluation of $p$ at $x$ via $f$ is zero, then the evaluation of $q$ at $x$ via $f$ is also zero. In other words, if $p \mid q$ and $\text{eval}_2(f, x)(p) = 0$, then $\text{eval}_2(f, x)(q) = 0$.
Polynomial.eval₂_list_prod theorem
(l : List R[X]) (x : S) : eval₂ f x l.prod = (l.map (eval₂ f x)).prod
Full source 
theorem eval₂_list_prod (l : List R[X]) (x : S) : eval₂ f x l.prod = (l.map (eval₂ f x)).prod :=
  map_list_prod (eval₂RingHom f x) l
Evaluation of Polynomial Product via Ring Homomorphism: $\text{eval}_2(f, x)(\prod p) = \prod \text{eval}_2(f, x)(p)$
Informal description
Let $R$ be a semiring and $S$ be a commutative semiring. Given a ring homomorphism $f \colon R \to S$ and an element $x \in S$, for any list $l$ of polynomials in $R[X]$, the evaluation of the product of $l$ at $x$ via $f$ equals the product of the evaluations of each polynomial in $l$ at $x$ via $f$. That is, \[ \text{eval}_2(f, x)\left(\prod_{p \in l} p\right) = \prod_{p \in l} \text{eval}_2(f, x)(p). \]
Polynomial.eval definition
: R → R[X] → R
Full source 
/-- `eval x p` is the evaluation of the polynomial `p` at `x` -/
def eval : R → R[X] → R :=
  eval₂ (RingHom.id _)
Evaluation of a polynomial at a point
Informal description
Given a polynomial $p \in R[X]$ and an element $x \in R$, the evaluation of $p$ at $x$ is defined as $\sum_{e} a_e \cdot x^e$, where $a_e$ are the coefficients of $p$. This is equivalent to evaluating $p$ via the identity ring homomorphism on $R$.
Polynomial.eval_eq_sum theorem
: p.eval x = p.sum fun e a => a * x ^ e
Full source 
theorem eval_eq_sum : p.eval x = p.sum fun e a => a * x ^ e := by
  rw [eval, eval₂_eq_sum]
  rfl
Polynomial Evaluation as Sum of Scaled Powers: $p(x) = \sum_e a_e x^e$
Informal description
For any polynomial $p \in R[X]$ and element $x \in R$, the evaluation of $p$ at $x$ equals the sum $\sum_{e} a_e \cdot x^e$, where $a_e$ are the coefficients of $p$.
Polynomial.eval₂_at_apply theorem
{S : Type*} [Semiring S] (f : R →+* S) (r : R) : p.eval₂ f (f r) = f (p.eval r)
Full source 
@[simp]
theorem eval₂_at_apply {S : Type*} [Semiring S] (f : R →+* S) (r : R) :
    p.eval₂ f (f r) = f (p.eval r) := by
  rw [eval₂_eq_sum, eval_eq_sum, sum, sum, map_sum f]
  simp only [f.map_mul, f.map_pow]
Evaluation via Ring Homomorphism: $\text{eval}_2(f, f(r), p) = f(p(r))$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $p \in R[X]$ a polynomial, and $r \in R$ an element. Then evaluating $p$ at $f(r)$ via $f$ equals $f$ applied to evaluating $p$ at $r$, i.e., \[ \text{eval}_2(f, f(r), p) = f(\text{eval}(r, p)). \]
Polynomial.eval₂_at_one theorem
{S : Type*} [Semiring S] (f : R →+* S) : p.eval₂ f 1 = f (p.eval 1)
Full source 
@[simp]
theorem eval₂_at_one {S : Type*} [Semiring S] (f : R →+* S) : p.eval₂ f 1 = f (p.eval 1) := by
  convert eval₂_at_apply (p := p) f 1
  simp
Evaluation at One via Ring Homomorphism: $\text{eval}_2(f, 1, p) = f(p(1))$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial. Then evaluating $p$ at $1 \in S$ via $f$ equals $f$ applied to evaluating $p$ at $1 \in R$, i.e., \[ \text{eval}_2(f, 1, p) = f(p(1)). \]
Polynomial.eval₂_at_natCast theorem
{S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) : p.eval₂ f n = f (p.eval n)
Full source 
@[simp]
theorem eval₂_at_natCast {S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) :
    p.eval₂ f n = f (p.eval n) := by
  convert eval₂_at_apply (p := p) f n
  simp
Evaluation of Polynomial at Natural Number via Ring Homomorphism: $\text{eval}_2(f, n, p) = f(p(n))$
Informal description
Let $R$ and $S$ be semirings, $f \colon R \to S$ a ring homomorphism, $p \in R[X]$ a polynomial, and $n \in \mathbb{N}$ a natural number. Then evaluating $p$ at $n$ via $f$ equals $f$ applied to evaluating $p$ at $n$, i.e., \[ \text{eval}_2(f, n, p) = f(\text{eval}(n, p)). \]
Polynomial.eval₂_at_ofNat theorem
{S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] : p.eval₂ f ofNat(n) = f (p.eval (ofNat(n)))
Full source 
@[simp]
theorem eval₂_at_ofNat {S : Type*} [Semiring S] (f : R →+* S) (n : ℕ) [n.AtLeastTwo] :
    p.eval₂ f ofNat(n) = f (p.eval (ofNat(n))) := by
  simp [OfNat.ofNat]
Evaluation of Polynomial at Numerals ≥ 2 via Ring Homomorphism: $\text{eval}_2(f, n, p) = f(p(n))$
Informal description
Let $R$ and $S$ be semirings, $f \colon R \to S$ a ring homomorphism, $p \in R[X]$ a polynomial, and $n \geq 2$ a natural number. Then evaluating $p$ at the numeral $n$ in $S$ via $f$ equals $f$ applied to evaluating $p$ at the numeral $n$ in $R$, i.e., \[ \text{eval}_2(f, n, p) = f(\text{eval}(n, p)). \]
Polynomial.eval_C theorem
: (C a).eval x = a
Full source 
@[simp]
theorem eval_C : (C a).eval x = a :=
  eval₂_C _ _
Evaluation of Constant Polynomial: $(C(a))(x) = a$
Informal description
For any element $a$ in a semiring $R$ and any element $x \in R$, the evaluation of the constant polynomial $C(a)$ at $x$ is equal to $a$, i.e., $(C(a)).\text{eval}(x) = a$.
Polynomial.eval_natCast theorem
{n : ℕ} : (n : R[X]).eval x = n
Full source 
@[simp]
theorem eval_natCast {n : ℕ} : (n : R[X]).eval x = n := by simp only [← C_eq_natCast, eval_C]
Evaluation of Constant Natural Number Polynomial: $(n)(x) = n$
Informal description
For any natural number $n$ and any element $x$ in a semiring $R$, the evaluation of the constant polynomial $n$ (viewed as an element of $R[X]$) at $x$ is equal to $n$.
Polynomial.eval_ofNat theorem
(n : ℕ) [n.AtLeastTwo] (a : R) : (ofNat(n) : R[X]).eval a = ofNat(n)
Full source 
@[simp]
lemma eval_ofNat (n : ℕ) [n.AtLeastTwo] (a : R) :
    (ofNat(n) : R[X]).eval a = ofNat(n) := by
  simp only [OfNat.ofNat, eval_natCast]
Evaluation of Constant Polynomial $(n)(a) = n$ for $n \geq 2$
Informal description
For any natural number $n \geq 2$ and any element $a$ in a semiring $R$, the evaluation of the constant polynomial $n$ (viewed as an element of $R[X]$) at $a$ is equal to $n$.
Polynomial.eval_X theorem
: X.eval x = x
Full source 
@[simp]
theorem eval_X : X.eval x = x :=
  eval₂_X _ _
Evaluation of Polynomial Variable $X$ at Point $x$ Yields $x$
Informal description
For any element $x$ in a semiring $R$, the evaluation of the polynomial variable $X$ at $x$ equals $x$, i.e., $\text{eval}(x, X) = x$.
Polynomial.eval_monomial theorem
{n a} : (monomial n a).eval x = a * x ^ n
Full source 
@[simp]
theorem eval_monomial {n a} : (monomial n a).eval x = a * x ^ n :=
  eval₂_monomial _ _
Evaluation of Monomial: $(aX^n)(x) = a x^n$
Informal description
For any natural number $n$, element $a \in R$, and element $x \in R$, the evaluation of the monomial $aX^n$ at $x$ is equal to $a \cdot x^n$.
Polynomial.eval_zero theorem
: (0 : R[X]).eval x = 0
Full source 
@[simp]
theorem eval_zero : (0 : R[X]).eval x = 0 :=
  eval₂_zero _ _
Evaluation of Zero Polynomial Yields Zero
Informal description
For any semiring $R$ and any element $x \in R$, the evaluation of the zero polynomial $0 \in R[X]$ at $x$ is equal to the zero element of $R$, i.e., $\text{eval}(x, 0) = 0$.
Polynomial.eval_add theorem
: (p + q).eval x = p.eval x + q.eval x
Full source 
@[simp]
theorem eval_add : (p + q).eval x = p.eval x + q.eval x :=
  eval₂_add _ _
Additivity of Polynomial Evaluation: $(p + q)(x) = p(x) + q(x)$
Informal description
For any polynomials $p, q \in R[X]$ and any element $x \in R$, the evaluation of the sum $p + q$ at $x$ is equal to the sum of the evaluations of $p$ and $q$ at $x$, i.e., \[ (p + q)(x) = p(x) + q(x). \]
Polynomial.eval_one theorem
: (1 : R[X]).eval x = 1
Full source 
@[simp]
theorem eval_one : (1 : R[X]).eval x = 1 :=
  eval₂_one _ _
Evaluation of the Constant Polynomial One: $1(x) = 1$
Informal description
For any element $x$ in a semiring $R$, the evaluation of the constant polynomial $1 \in R[X]$ at $x$ is equal to the multiplicative identity $1 \in R$, i.e., $1(x) = 1$.
Polynomial.eval_C_mul theorem
: (C a * p).eval x = a * p.eval x
Full source 
@[simp]
theorem eval_C_mul : (C a * p).eval x = a * p.eval x := by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, eval_add, ph, qh]
  | monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]
Evaluation of Constant Multiple: $(C(a) \cdot p)(x) = a \cdot p(x)$
Informal description
For any polynomial $p \in R[X]$, any element $a \in R$, and any element $x \in R$, the evaluation of the product of the constant polynomial $C(a)$ and $p$ at $x$ is equal to $a$ multiplied by the evaluation of $p$ at $x$, i.e., $$(C(a) \cdot p)(x) = a \cdot p(x).$$
Polynomial.eval_natCast_mul theorem
{n : ℕ} : ((n : R[X]) * p).eval x = n * p.eval x
Full source 
@[simp]
theorem eval_natCast_mul {n : ℕ} : ((n : R[X]) * p).eval x = n * p.eval x := by
  rw [← C_eq_natCast, eval_C_mul]
Evaluation of Natural Number Multiple: $(n \cdot p)(x) = n \cdot p(x)$
Informal description
For any natural number $n$, polynomial $p \in R[X]$, and element $x \in R$, the evaluation of the product $(n \cdot p)$ at $x$ equals $n$ multiplied by the evaluation of $p$ at $x$, i.e., $$ (n \cdot p)(x) = n \cdot p(x). $$
Polynomial.eval_mul_X theorem
: (p * X).eval x = p.eval x * x
Full source 
@[simp]
theorem eval_mul_X : (p * X).eval x = p.eval x * x := by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [add_mul, eval_add, ph, qh]
  | monomial n a =>
    simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ,
      mul_assoc]
Evaluation of $p \cdot X$: $(p \cdot X)(x) = p(x) \cdot x$
Informal description
For any polynomial $p \in R[X]$ and any element $x \in R$, the evaluation of the product $p \cdot X$ at $x$ equals the evaluation of $p$ at $x$ multiplied by $x$, i.e., $$ (p \cdot X)(x) = p(x) \cdot x. $$
Polynomial.eval_mul_X_pow theorem
{k : ℕ} : (p * X ^ k).eval x = p.eval x * x ^ k
Full source 
@[simp]
theorem eval_mul_X_pow {k : ℕ} : (p * X ^ k).eval x = p.eval x * x ^ k := by
  induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, ← mul_assoc, ih]
Evaluation of $p \cdot X^k$: $(p \cdot X^k)(x) = p(x) \cdot x^k$
Informal description
For any polynomial $p \in R[X]$, any natural number $k \in \mathbb{N}$, and any element $x \in R$, the evaluation of the product $p \cdot X^k$ at $x$ equals the evaluation of $p$ at $x$ multiplied by $x^k$, i.e., $$ (p \cdot X^k)(x) = p(x) \cdot x^k. $$
Polynomial.eval_sum theorem
(p : R[X]) (f : ℕ → R → R[X]) (x : R) : (p.sum f).eval x = p.sum fun n a => (f n a).eval x
Full source 
theorem eval_sum (p : R[X]) (f : ℕ → R → R[X]) (x : R) :
    (p.sum f).eval x = p.sum fun n a => (f n a).eval x :=
  eval₂_sum _ _ _ _
Linearity of Polynomial Evaluation over Sums
Informal description
For any polynomial $p \in R[X]$, any function $f \colon \mathbb{N} \to R \to R[X]$, and any element $x \in R$, the evaluation of the sum polynomial $\sum_{n} f(n, a_n)$ at $x$ equals the sum of the evaluations of each $f(n, a_n)$ at $x$. That is, \[ \left( \sum_{n} f(n, a_n) \right)(x) = \sum_{n} (f(n, a_n))(x). \]
Polynomial.eval_finset_sum theorem
(s : Finset ι) (g : ι → R[X]) (x : R) : (∑ i ∈ s, g i).eval x = ∑ i ∈ s, (g i).eval x
Full source 
theorem eval_finset_sum (s : Finset ι) (g : ι → R[X]) (x : R) :
    (∑ i ∈ s, g i).eval x = ∑ i ∈ s, (g i).eval x :=
  eval₂_finset_sum _ _ _ _
Linearity of Polynomial Evaluation over Finite Sums
Informal description
For any finite set $s$ of indices, any family of polynomials $(g_i)_{i \in s}$ in $R[X]$, and any element $x \in R$, the evaluation of the sum $\sum_{i \in s} g_i$ at $x$ equals the sum of the evaluations of each $g_i$ at $x$. That is, $$\left(\sum_{i \in s} g_i\right)(x) = \sum_{i \in s} g_i(x).$$
Polynomial.IsRoot definition
(p : R[X]) (a : R) : Prop
Full source 
/-- `IsRoot p x` implies `x` is a root of `p`. The evaluation of `p` at `x` is zero -/
def IsRoot (p : R[X]) (a : R) : Prop :=
  p.eval a = 0
Root of a polynomial
Informal description
Given a polynomial $p \in R[X]$ and an element $a \in R$, we say that $a$ is a root of $p$ if the evaluation of $p$ at $a$ is zero, i.e., $p(a) = 0$.
Polynomial.IsRoot.decidable instance
[DecidableEq R] : Decidable (IsRoot p a)
Full source 
instance IsRoot.decidable [DecidableEq R] : Decidable (IsRoot p a) := by
  unfold IsRoot; infer_instance
Decidability of Polynomial Roots in Semirings with Decidable Equality
Informal description
For any polynomial $p \in R[X]$ and element $a \in R$ in a semiring $R$ with decidable equality, it is decidable whether $a$ is a root of $p$ (i.e., whether $p(a) = 0$).
Polynomial.IsRoot.def theorem
: IsRoot p a ↔ p.eval a = 0
Full source 
@[simp]
theorem IsRoot.def : IsRootIsRoot p a ↔ p.eval a = 0 :=
  Iff.rfl
Characterization of Polynomial Roots via Evaluation
Informal description
For a polynomial $p \in R[X]$ and an element $a \in R$, $a$ is a root of $p$ if and only if the evaluation of $p$ at $a$ is zero, i.e., $p(a) = 0$.
Polynomial.IsRoot.dvd theorem
{R : Type*} [CommSemiring R] {p q : R[X]} {x : R} (h : p.IsRoot x) (hpq : p ∣ q) : q.IsRoot x
Full source 
theorem IsRoot.dvd {R : Type*} [CommSemiring R] {p q : R[X]} {x : R} (h : p.IsRoot x)
    (hpq : p ∣ q) : q.IsRoot x := by
  rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]
Root Preservation Under Divisibility in Polynomials
Informal description
Let $R$ be a commutative semiring, $p, q \in R[X]$ be polynomials, and $x \in R$. If $x$ is a root of $p$ (i.e., $p(x) = 0$) and $p$ divides $q$, then $x$ is also a root of $q$ (i.e., $q(x) = 0$).
Polynomial.not_isRoot_C theorem
(r a : R) (hr : r ≠ 0) : ¬IsRoot (C r) a
Full source 
theorem not_isRoot_C (r a : R) (hr : r ≠ 0) : ¬IsRoot (C r) a := by simpa using hr
Nonzero Constant Polynomials Have No Roots
Informal description
For any elements $r, a$ in a semiring $R$, if $r \neq 0$, then $a$ is not a root of the constant polynomial $C(r)$, i.e., $C(r)(a) \neq 0$.
Polynomial.eval_surjective theorem
(x : R) : Function.Surjective <| eval x
Full source 
theorem eval_surjective (x : R) : Function.Surjective <| eval x := fun y => ⟨C y, eval_C⟩
Surjectivity of Polynomial Evaluation at Any Point
Informal description
For any element $x$ in a semiring $R$, the polynomial evaluation function $\text{eval}(x) : R[X] \to R$ is surjective. That is, for every $a \in R$, there exists a polynomial $p \in R[X]$ such that $p(x) = a$.
Polynomial.comp definition
(p q : R[X]) : R[X]
Full source 
/-- The composition of polynomials as a polynomial. -/
def comp (p q : R[X]) : R[X] :=
  p.eval₂ C q
Polynomial composition
Informal description
Given two polynomials $p, q \in R[X]$, the composition $p \circ q$ is defined as the evaluation of $p$ at $q$ via the constant polynomial embedding $C: R \to R[X]$. In other words, it is the polynomial obtained by substituting $q$ into $p$ as the variable.
Polynomial.comp_eq_sum_left theorem
: p.comp q = p.sum fun e a => C a * q ^ e
Full source 
theorem comp_eq_sum_left : p.comp q = p.sum fun e a => C a * q ^ e := by rw [comp, eval₂_eq_sum]
Polynomial Composition as Sum of Scaled Powers: $p \circ q = \sum_e a_e q^e$
Informal description
For any polynomials $p, q \in R[X]$, the composition $p \circ q$ is equal to the sum $\sum_{e} C(a_e) \cdot q^e$, where $a_e$ are the coefficients of $p$.
Polynomial.comp_X theorem
: p.comp X = p
Full source 
@[simp]
theorem comp_X : p.comp X = p := by
  simp only [comp, eval₂_def, C_mul_X_pow_eq_monomial]
  exact sum_monomial_eq _
Composition with X Preserves Polynomial Identity
Informal description
For any polynomial $p \in R[X]$, the composition of $p$ with the polynomial variable $X$ is equal to $p$ itself, i.e., $p \circ X = p$.
Polynomial.X_comp theorem
: X.comp p = p
Full source 
@[simp]
theorem X_comp : X.comp p = p :=
  eval₂_X _ _
Composition of $X$ with a Polynomial Yields the Polynomial Itself
Informal description
For any polynomial $p \in R[X]$, the composition of the polynomial variable $X$ with $p$ is equal to $p$, i.e., $X \circ p = p$.
Polynomial.comp_C theorem
: p.comp (C a) = C (p.eval a)
Full source 
@[simp]
theorem comp_C : p.comp (C a) = C (p.eval a) := by simp [comp, map_sum (C : R →+* _)]
Composition with Constant Polynomial: $p \circ C(a) = C(p(a))$
Informal description
For any polynomial $p \in R[X]$ and any element $a \in R$, the composition of $p$ with the constant polynomial $C(a)$ is equal to the constant polynomial whose coefficient is the evaluation of $p$ at $a$, i.e., \[ p \circ C(a) = C(p(a)). \]
Polynomial.C_comp theorem
: (C a).comp p = C a
Full source 
@[simp]
theorem C_comp : (C a).comp p = C a :=
  eval₂_C _ _
Composition of Constant Polynomial Preserves Identity: $(C(a)) \circ p = C(a)$
Informal description
For any element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the composition of the constant polynomial $C(a)$ with $p$ is equal to $C(a)$ itself, i.e., $(C(a)) \circ p = C(a)$.
Polynomial.natCast_comp theorem
{n : ℕ} : (n : R[X]).comp p = n
Full source 
@[simp]
theorem natCast_comp {n : ℕ} : (n : R[X]).comp p = n := by rw [← C_eq_natCast, C_comp]
Composition of Natural Number Cast with Polynomial Preserves Identity: $(n) \circ p = n$
Informal description
For any natural number $n$ and polynomial $p \in R[X]$, the composition of the constant polynomial $n$ with $p$ is equal to $n$ itself, i.e., $(n : R[X]) \circ p = n$.
Polynomial.ofNat_comp theorem
(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R[X]).comp p = n
Full source 
@[simp]
theorem ofNat_comp (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R[X]).comp p = n :=
  natCast_comp
Composition with Numerals $\geq 2$ Preserves Identity: $(n) \circ p = n$
Informal description
For any natural number $n \geq 2$ and any polynomial $p \in R[X]$, the composition of the constant polynomial $n$ with $p$ is equal to $n$ itself, i.e., $(n : R[X]) \circ p = n$.
Polynomial.comp_zero theorem
: p.comp (0 : R[X]) = C (p.eval 0)
Full source 
@[simp]
theorem comp_zero : p.comp (0 : R[X]) = C (p.eval 0) := by rw [← C_0, comp_C]
Composition with Zero Polynomial: $p \circ 0 = C(p(0))$
Informal description
For any polynomial $p \in R[X]$, the composition of $p$ with the zero polynomial $0 \in R[X]$ is equal to the constant polynomial whose coefficient is the evaluation of $p$ at $0$, i.e., \[ p \circ 0 = C(p(0)). \]
Polynomial.zero_comp theorem
: comp (0 : R[X]) p = 0
Full source 
@[simp]
theorem zero_comp : comp (0 : R[X]) p = 0 := by rw [← C_0, C_comp]
Composition with Zero Polynomial Yields Zero
Informal description
For any polynomial $p \in R[X]$, the composition of the zero polynomial $0 \in R[X]$ with $p$ is equal to the zero polynomial, i.e., $0 \circ p = 0$.
Polynomial.comp_one theorem
: p.comp 1 = C (p.eval 1)
Full source 
@[simp]
theorem comp_one : p.comp 1 = C (p.eval 1) := by rw [← C_1, comp_C]
Composition with One: $p \circ 1 = C(p(1))$
Informal description
For any polynomial $p \in R[X]$, the composition of $p$ with the constant polynomial $1$ is equal to the constant polynomial whose coefficient is the evaluation of $p$ at $1$, i.e., \[ p \circ 1 = C(p(1)). \]
Polynomial.one_comp theorem
: comp (1 : R[X]) p = 1
Full source 
@[simp]
theorem one_comp : comp (1 : R[X]) p = 1 := by rw [← C_1, C_comp]
Composition of One Polynomial: $1 \circ p = 1$
Informal description
For any polynomial $p \in R[X]$, the composition of the constant polynomial $1$ with $p$ is equal to $1$, i.e., $1 \circ p = 1$.
Polynomial.add_comp theorem
: (p + q).comp r = p.comp r + q.comp r
Full source 
@[simp]
theorem add_comp : (p + q).comp r = p.comp r + q.comp r :=
  eval₂_add _ _
Additivity of Polynomial Composition: $(p + q) \circ r = p \circ r + q \circ r$
Informal description
For any polynomials $p, q, r \in R[X]$, the composition of the sum $p + q$ with $r$ is equal to the sum of the compositions of $p$ with $r$ and $q$ with $r$, i.e., $$(p + q) \circ r = p \circ r + q \circ r.$$
Polynomial.monomial_comp theorem
(n : ℕ) : (monomial n a).comp p = C a * p ^ n
Full source 
@[simp]
theorem monomial_comp (n : ℕ) : (monomial n a).comp p = C a * p ^ n :=
  eval₂_monomial _ _
Composition of Monomial with Polynomial: $(aX^n) \circ p = a \cdot p^n$
Informal description
For any natural number $n$ and coefficient $a \in R$, the composition of the monomial $aX^n$ with a polynomial $p \in R[X]$ is equal to the constant polynomial $a$ multiplied by $p$ raised to the power $n$, i.e., $(aX^n) \circ p = a \cdot p^n$.
Polynomial.mul_X_comp theorem
: (p * X).comp r = p.comp r * r
Full source 
@[simp]
theorem mul_X_comp : (p * X).comp r = p.comp r * r := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, add_mul, add_comp]
  | monomial n b => simp only [pow_succ, mul_assoc, monomial_mul_X, monomial_comp]
Composition of Polynomial Product with $X$: $(p \cdot X) \circ r = (p \circ r) \cdot r$
Informal description
For any polynomials $p, r \in R[X]$, the composition of the product $p \cdot X$ with $r$ is equal to the composition of $p$ with $r$ multiplied by $r$, i.e., $$(p \cdot X) \circ r = (p \circ r) \cdot r.$$
Polynomial.X_pow_comp theorem
{k : ℕ} : (X ^ k).comp p = p ^ k
Full source 
@[simp]
theorem X_pow_comp {k : ℕ} : (X ^ k).comp p = p ^ k := by
  induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, mul_X_comp, ih]
Composition of $X^k$ with $p$: $(X^k) \circ p = p^k$
Informal description
For any natural number $k$ and any polynomial $p \in R[X]$, the composition of the monomial $X^k$ with $p$ is equal to $p$ raised to the power $k$, i.e., $$(X^k) \circ p = p^k.$$
Polynomial.mul_X_pow_comp theorem
{k : ℕ} : (p * X ^ k).comp r = p.comp r * r ^ k
Full source 
@[simp]
theorem mul_X_pow_comp {k : ℕ} : (p * X ^ k).comp r = p.comp r * r ^ k := by
  induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, mul_X_comp]
Composition of Polynomial Product with $X^k$: $(p \cdot X^k) \circ r = (p \circ r) \cdot r^k$
Informal description
For any natural number $k$ and polynomials $p, r \in R[X]$, the composition of the product $p \cdot X^k$ with $r$ is equal to the composition of $p$ with $r$ multiplied by $r^k$, i.e., $$(p \cdot X^k) \circ r = (p \circ r) \cdot r^k.$$
Polynomial.C_mul_comp theorem
: (C a * p).comp r = C a * p.comp r
Full source 
@[simp]
theorem C_mul_comp : (C a * p).comp r = C a * p.comp r := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq, mul_add]
  | monomial n b => simp [mul_assoc]
Composition of Constant Multiple: $(a \cdot p) \circ r = a \cdot (p \circ r)$
Informal description
For any element $a$ in a semiring $R$ and any polynomials $p, r \in R[X]$, the composition of the product of the constant polynomial $C(a)$ and $p$ with $r$ is equal to the product of $C(a)$ and the composition of $p$ with $r$, i.e., $$(a \cdot p) \circ r = a \cdot (p \circ r).$$
Polynomial.natCast_mul_comp theorem
{n : ℕ} : ((n : R[X]) * p).comp r = n * p.comp r
Full source 
@[simp]
theorem natCast_mul_comp {n : ℕ} : ((n : R[X]) * p).comp r = n * p.comp r := by
  rw [← C_eq_natCast, C_mul_comp]
Composition of Natural Number Multiple: $(n \cdot p) \circ r = n \cdot (p \circ r)$
Informal description
For any natural number $n$ and polynomials $p, r \in R[X]$, the composition of the product of the constant polynomial $n$ and $p$ with $r$ is equal to the product of $n$ and the composition of $p$ with $r$, i.e., $$(n \cdot p) \circ r = n \cdot (p \circ r).$$
Polynomial.mul_X_add_natCast_comp theorem
{n : ℕ} : (p * (X + (n : R[X]))).comp q = p.comp q * (q + n)
Full source 
theorem mul_X_add_natCast_comp {n : ℕ} :
    (p * (X + (n : R[X]))).comp q = p.comp q * (q + n) := by
  rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
Composition of Polynomial Product with $X + n$: $(p \cdot (X + n)) \circ q = (p \circ q) \cdot (q + n)$
Informal description
For any natural number $n$ and polynomials $p, q \in R[X]$, the composition of the product $p \cdot (X + n)$ with $q$ is equal to the product of the composition of $p$ with $q$ and the polynomial $(q + n)$, i.e., $$(p \cdot (X + n)) \circ q = (p \circ q) \cdot (q + n).$$
Polynomial.mul_comp theorem
{R : Type*} [CommSemiring R] (p q r : R[X]) : (p * q).comp r = p.comp r * q.comp r
Full source 
@[simp]
theorem mul_comp {R : Type*} [CommSemiring R] (p q r : R[X]) :
    (p * q).comp r = p.comp r * q.comp r :=
  eval₂_mul _ _
Composition Distributes over Polynomial Multiplication
Informal description
Let $R$ be a commutative semiring and let $p, q, r \in R[X]$ be polynomials. Then the composition of the product $p \cdot q$ with $r$ is equal to the product of the compositions of $p$ and $q$ with $r$, i.e., $$(p \cdot q) \circ r = (p \circ r) \cdot (q \circ r).$$
Polynomial.pow_comp theorem
{R : Type*} [CommSemiring R] (p q : R[X]) (n : ℕ) : (p ^ n).comp q = p.comp q ^ n
Full source 
@[simp]
theorem pow_comp {R : Type*} [CommSemiring R] (p q : R[X]) (n : ℕ) :
    (p ^ n).comp q = p.comp q ^ n :=
  (MonoidHom.mk (OneHom.mk (fun r : R[X] => r.comp q) one_comp) fun r s => mul_comp r s q).map_pow
    p n
Power of Polynomial Composition: $(p^n) \circ q = (p \circ q)^n$
Informal description
Let $R$ be a commutative semiring and let $p, q \in R[X]$ be polynomials. For any natural number $n$, the composition of the power $p^n$ with $q$ is equal to the power of the composition of $p$ with $q$, i.e., $$(p^n) \circ q = (p \circ q)^n.$$
Polynomial.comp_assoc theorem
{R : Type*} [CommSemiring R] (φ ψ χ : R[X]) : (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
Full source 
theorem comp_assoc {R : Type*} [CommSemiring R] (φ ψ χ : R[X]) :
    (φ.comp ψ).comp χ = φ.comp (ψ.comp χ) := by
  refine Polynomial.induction_on φ ?_ ?_ ?_ <;>
    · intros
      simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]
Associativity of Polynomial Composition
Informal description
Let $R$ be a commutative semiring and let $\varphi, \psi, \chi \in R[X]$ be polynomials. Then the composition of polynomials is associative, i.e., $$(\varphi \circ \psi) \circ \chi = \varphi \circ (\psi \circ \chi).$$
Polynomial.sum_comp theorem
(s : Finset ι) (p : ι → R[X]) (q : R[X]) : (∑ i ∈ s, p i).comp q = ∑ i ∈ s, (p i).comp q
Full source 
@[simp] lemma sum_comp (s : Finset ι) (p : ι → R[X]) (q : R[X]) :
    (∑ i ∈ s, p i).comp q = ∑ i ∈ s, (p i).comp q := Polynomial.eval₂_finset_sum _ _ _ _
Sum of Polynomial Compositions Equals Composition of Sum
Informal description
Let $R$ be a commutative semiring, $s$ a finite set of indices, $(p_i)_{i \in s}$ a family of polynomials in $R[X]$, and $q \in R[X]$. Then the composition of the sum $\sum_{i \in s} p_i$ with $q$ equals the sum of the compositions of each $p_i$ with $q$: $$\left(\sum_{i \in s} p_i\right) \circ q = \sum_{i \in s} (p_i \circ q)$$
Polynomial.map definition
: R[X] → S[X]
Full source 
/-- `map f p` maps a polynomial `p` across a ring hom `f` -/
def map : R[X] → S[X] :=
  eval₂ (C.comp f) X
Polynomial coefficient mapping via a ring homomorphism
Informal description
Given a ring homomorphism $f \colon R \to S$, the function `Polynomial.map` transforms a polynomial $p \in R[X]$ into a polynomial in $S[X]$ by applying $f$ to each coefficient of $p$. Specifically, if $p = \sum_{i=0}^n a_i X^i$, then $\text{map}\, f\, p = \sum_{i=0}^n f(a_i) X^i$.
Polynomial.map_C theorem
: (C a).map f = C (f a)
Full source 
@[simp]
theorem map_C : (C a).map f = C (f a) :=
  eval₂_C _ _
Mapping of Constant Polynomials: $\text{map}\, f\, (C(a)) = C(f(a))$
Informal description
For any semiring homomorphism $f \colon R \to S$ and any element $a \in R$, the image of the constant polynomial $C(a)$ under the polynomial map induced by $f$ is the constant polynomial $C(f(a))$, i.e., \[ \text{map}\, f\, (C(a)) = C(f(a)). \]
Polynomial.map_X theorem
: X.map f = X
Full source 
@[simp]
theorem map_X : X.map f = X :=
  eval₂_X _ _
Invariance of Polynomial Variable $X$ under Coefficient Mapping
Informal description
For any ring homomorphism $f \colon R \to S$, the image of the polynomial variable $X$ under the coefficient mapping is $X$ itself, i.e., $f(X) = X$.
Polynomial.map_monomial theorem
{n a} : (monomial n a).map f = monomial n (f a)
Full source 
@[simp]
theorem map_monomial {n a} : (monomial n a).map f = monomial n (f a) := by
  dsimp only [map]
  rw [eval₂_monomial, ← C_mul_X_pow_eq_monomial]; rfl
Monomial Coefficient Mapping via Ring Homomorphism: $\text{map}\, f\, (aX^n) = f(a)X^n$
Informal description
For any natural number $n$, element $a \in R$, and ring homomorphism $f \colon R \to S$, the coefficient mapping of the monomial $aX^n$ under $f$ is equal to the monomial $(f(a))X^n$ in $S[X]$. That is, \[ \text{map}\, f\, (aX^n) = f(a)X^n. \]
Polynomial.map_zero theorem
: (0 : R[X]).map f = 0
Full source 
@[simp]
protected theorem map_zero : (0 : R[X]).map f = 0 :=
  eval₂_zero _ _
Coefficient Mapping Preserves Zero Polynomial
Informal description
For any ring homomorphism $f \colon R \to S$, the image of the zero polynomial under the coefficient mapping is the zero polynomial in $S[X]$, i.e., $f(0) = 0$.
Polynomial.map_add theorem
: (p + q).map f = p.map f + q.map f
Full source 
@[simp]
protected theorem map_add : (p + q).map f = p.map f + q.map f :=
  eval₂_add _ _
Additivity of Polynomial Coefficient Mapping via Ring Homomorphism
Informal description
For any polynomials $p, q \in R[X]$ and a ring homomorphism $f \colon R \to S$, the map of the sum $p + q$ under $f$ is equal to the sum of the maps of $p$ and $q$ under $f$. That is, \[ \text{map}\, f\, (p + q) = \text{map}\, f\, p + \text{map}\, f\, q. \]
Polynomial.map_one theorem
: (1 : R[X]).map f = 1
Full source 
@[simp]
protected theorem map_one : (1 : R[X]).map f = 1 :=
  eval₂_one _ _
Coefficient Mapping Preserves Multiplicative Identity Polynomial
Informal description
For any ring homomorphism $f \colon R \to S$, the image of the constant polynomial $1 \in R[X]$ under the coefficient mapping is the constant polynomial $1 \in S[X]$, i.e., $\text{map}_f(1) = 1$.
Polynomial.map_mul theorem
: (p * q).map f = p.map f * q.map f
Full source 
@[simp]
protected theorem map_mul : (p * q).map f = p.map f * q.map f := by
  rw [map, eval₂_mul_noncomm]
  exact fun k => (commute_X _).symm
Multiplicativity of Polynomial Coefficient Mapping via Ring Homomorphism
Informal description
For any polynomials $p, q \in R[X]$ and a ring homomorphism $f \colon R \to S$, the map of the product $p \cdot q$ under $f$ is equal to the product of the maps of $p$ and $q$ under $f$. That is, \[ \text{map}_f(p \cdot q) = \text{map}_f(p) \cdot \text{map}_f(q). \]
Polynomial.mapRingHom definition
(f : R →+* S) : R[X] →+* S[X]
Full source 
/-- `Polynomial.map` as a `RingHom`. -/
def mapRingHom (f : R →+* S) : R[X]R[X] →+* S[X] where
  toFun := Polynomial.map f
  map_add' _ _ := Polynomial.map_add f
  map_zero' := Polynomial.map_zero f
  map_mul' _ _ := Polynomial.map_mul f
  map_one' := Polynomial.map_one f
Polynomial coefficient mapping ring homomorphism
Informal description
Given a ring homomorphism $f \colon R \to S$, the function `Polynomial.mapRingHom` is the bundled ring homomorphism that maps a polynomial $p \in R[X]$ to a polynomial in $S[X]$ by applying $f$ to each coefficient of $p$. Specifically, if $p = \sum_{i=0}^n a_i X^i$, then $\text{mapRingHom}\, f\, p = \sum_{i=0}^n f(a_i) X^i$. This function preserves addition, multiplication, zero, and one.
Polynomial.coe_mapRingHom theorem
(f : R →+* S) : ⇑(mapRingHom f) = map f
Full source 
@[simp]
theorem coe_mapRingHom (f : R →+* S) : ⇑(mapRingHom f) = map f :=
  rfl
Equality of Polynomial Coefficient Mapping Functions via Ring Homomorphism
Informal description
For any ring homomorphism $f \colon R \to S$, the underlying function of the polynomial coefficient mapping ring homomorphism $\text{mapRingHom}\, f \colon R[X] \to S[X]$ is equal to the polynomial coefficient mapping function $\text{map}\, f \colon R[X] \to S[X]$. In other words, the ring homomorphism $\text{mapRingHom}\, f$ acts on polynomials by applying $f$ to each coefficient, just like the function $\text{map}\, f$.
Polynomial.map_natCast theorem
(n : ℕ) : (n : R[X]).map f = n
Full source 
@[simp]
protected theorem map_natCast (n : ℕ) : (n : R[X]).map f = n :=
  map_natCast (mapRingHom f) n
Preservation of Natural Number Constants under Polynomial Mapping
Informal description
For any natural number $n$ and any ring homomorphism $f \colon R \to S$, the image of the constant polynomial $n$ under the coefficient mapping $f$ is equal to $n$ itself, i.e., $f(n) = n$.
Polynomial.map_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R[X]).map f = ofNat(n)
Full source 
@[simp]
protected theorem map_ofNat (n : ℕ) [n.AtLeastTwo] :
    (ofNat(n) : R[X]).map f = ofNat(n) :=
  show (n : R[X]).map f = n by rw [Polynomial.map_natCast]
Preservation of Numerals ≥ 2 under Polynomial Mapping
Informal description
For any natural number $n \geq 2$ and any ring homomorphism $f \colon R \to S$ between semirings $R$ and $S$, the image of the constant polynomial $n$ under the coefficient-wise map $f$ is equal to the constant polynomial $n$ in $S[X]$, i.e., \[ \text{map}\, f\, (n) = n. \]
Polynomial.map_dvd theorem
(f : R →+* S) {x y : R[X]} : x ∣ y → x.map f ∣ y.map f
Full source 
theorem map_dvd (f : R →+* S) {x y : R[X]} : x ∣ y → x.map f ∣ y.map f :=
  (mapRingHom f).map_dvd
Divisibility Preservation Under Polynomial Coefficient Mapping
Informal description
Let $f \colon R \to S$ be a ring homomorphism between semirings $R$ and $S$. For any polynomials $x, y \in R[X]$, if $x$ divides $y$ in $R[X]$, then the image of $x$ under the coefficient-wise map $f$ divides the image of $y$ under $f$ in $S[X]$.
Polynomial.mapRingHom_comp_C theorem
{R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) : (mapRingHom f).comp C = C.comp f
Full source 
lemma mapRingHom_comp_C {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) :
    (mapRingHom f).comp C = C.comp f := by ext; simp
Composition of Polynomial Mapping and Constant Homomorphism: $(\text{mapRingHom}\, f) \circ C = C \circ f$
Informal description
For any semirings $R$ and $S$ and any ring homomorphism $f \colon R \to S$, the composition of the polynomial coefficient mapping ring homomorphism $\text{mapRingHom}\, f$ with the constant polynomial homomorphism $C$ is equal to the composition of $C$ with $f$, i.e., \[ (\text{mapRingHom}\, f) \circ C = C \circ f. \]
Polynomial.eval₂_eq_eval_map theorem
{x : S} : p.eval₂ f x = (p.map f).eval x
Full source 
theorem eval₂_eq_eval_map {x : S} : p.eval₂ f x = (p.map f).eval x := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq]
  | monomial n r => simp
Equivalence of Evaluation via Ring Homomorphism and Mapped Polynomial Evaluation: $\text{eval}_2(f, x, p) = (\text{map}\, f\, p)(x)$
Informal description
For any polynomial $p \in R[X]$, ring homomorphism $f \colon R \to S$, and element $x \in S$, the evaluation of $p$ at $x$ via $f$ is equal to the evaluation of the mapped polynomial $p.map\, f$ at $x$ in $S[X]$. That is, \[ \text{eval}_2(f, x, p) = \text{eval}(x, \text{map}\, f\, p). \]
Polynomial.map_list_prod theorem
(L : List R[X]) : L.prod.map f = (L.map <| map f).prod
Full source 
protected theorem map_list_prod (L : List R[X]) : L.prod.map f = (L.map <| map f).prod :=
  Eq.symm <| List.prod_hom _ (mapRingHom f).toMonoidHom
Ring Homomorphism Preserves Polynomial List Products: $f(\prod p) = \prod f(p)$
Informal description
Let $R$ and $S$ be semirings and $f : R \to S$ be a ring homomorphism. For any list $L$ of polynomials in $R[X]$, the image under $f$ of the product of $L$ equals the product of the list obtained by applying the coefficient-wise map $f$ to each polynomial in $L$. That is, \[ f\left(\prod_{p \in L} p\right) = \prod_{p \in L} f(p). \]
Polynomial.map_pow theorem
(n : ℕ) : (p ^ n).map f = p.map f ^ n
Full source 
@[simp]
protected theorem map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n :=
  (mapRingHom f).map_pow _ _
Power Preservation under Polynomial Coefficient Mapping: $\text{map}\, f\, (p^n) = (\text{map}\, f\, p)^n$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $p \in R[X]$ a polynomial. For any natural number $n$, the map of $p^n$ under $f$ equals the $n$-th power of the map of $p$ under $f$, i.e., $$ \text{map}\, f\, (p^n) = (\text{map}\, f\, p)^n. $$
Polynomial.eval_map theorem
(x : S) : (p.map f).eval x = p.eval₂ f x
Full source 
theorem eval_map (x : S) : (p.map f).eval x = p.eval₂ f x :=
  (eval₂_eq_eval_map f).symm
Equality of Evaluation Methods for Mapped Polynomials: $\text{eval}(x, \text{map}\, f\, p) = \text{eval}_2(f, x, p)$
Informal description
For any polynomial $p \in R[X]$, ring homomorphism $f \colon R \to S$, and element $x \in S$, the evaluation of the mapped polynomial $p.map\, f$ at $x$ equals the evaluation of $p$ at $x$ via $f$. That is, \[ \text{eval}(x, \text{map}\, f\, p) = \text{eval}_2(f, x, p). \]
Polynomial.map_sum theorem
{ι : Type*} (g : ι → R[X]) (s : Finset ι) : (∑ i ∈ s, g i).map f = ∑ i ∈ s, (g i).map f
Full source 
protected theorem map_sum {ι : Type*} (g : ι → R[X]) (s : Finset ι) :
    (∑ i ∈ s, g i).map f = ∑ i ∈ s, (g i).map f :=
  map_sum (mapRingHom f) _ _
Linearity of Polynomial Coefficient Mapping over Finite Sums: $\text{map}\, f\, (\sum g_i) = \sum \text{map}\, f\, g_i$
Informal description
Let $R$ and $S$ be semirings, $f \colon R \to S$ a ring homomorphism, and $\{g_i\}_{i \in \iota}$ a family of polynomials in $R[X]$ indexed by a finite set $\iota$. For any finite subset $s \subseteq \iota$, the image under $f$ of the sum $\sum_{i \in s} g_i$ equals the sum of the images of the $g_i$ under $f$. That is, \[ \text{map}\, f \left( \sum_{i \in s} g_i \right) = \sum_{i \in s} \text{map}\, f\, g_i. \]
Polynomial.map_comp theorem
(p q : R[X]) : map f (p.comp q) = (map f p).comp (map f q)
Full source 
theorem map_comp (p q : R[X]) : map f (p.comp q) = (map f p).comp (map f q) :=
  Polynomial.induction_on p (by simp only [map_C, forall_const, C_comp, eq_self_iff_true])
    (by
      simp +contextual only [Polynomial.map_add, add_comp, forall_const,
        imp_true_iff, eq_self_iff_true])
    (by
      simp +contextual only [pow_succ, ← mul_assoc, comp, forall_const,
        eval₂_mul_X, imp_true_iff, eq_self_iff_true, map_X, Polynomial.map_mul])
Compatibility of Polynomial Composition with Coefficient Mapping: $\text{map}\, f\, (p \circ q) = (\text{map}\, f\, p) \circ (\text{map}\, f\, q)$
Informal description
For any polynomials $p, q \in R[X]$ and a ring homomorphism $f \colon R \to S$, the image of the composition $p \circ q$ under the coefficient mapping $f$ is equal to the composition of the images of $p$ and $q$ under $f$. That is, \[ \text{map}\, f\, (p \circ q) = (\text{map}\, f\, p) \circ (\text{map}\, f\, q). \]
Polynomial.eval_mul theorem
: (p * q).eval x = p.eval x * q.eval x
Full source 
@[simp]
theorem eval_mul : (p * q).eval x = p.eval x * q.eval x :=
  eval₂_mul _ _
Multiplicativity of Polynomial Evaluation: $(p \cdot q)(x) = p(x) \cdot q(x)$
Informal description
For any polynomials $p, q \in R[X]$ and any element $x \in R$, the evaluation of the product $p \cdot q$ at $x$ equals the product of the evaluations of $p$ and $q$ at $x$, i.e., $$(p \cdot q)(x) = p(x) \cdot q(x).$$
Polynomial.evalRingHom definition
: R → R[X] →+* R
Full source 
/-- `eval r`, regarded as a ring homomorphism from `R[X]` to `R`. -/
def evalRingHom : R → R[X]R[X] →+* R :=
  eval₂RingHom (RingHom.id _)
Ring homomorphism of polynomial evaluation at \( x \)
Informal description
The ring homomorphism that evaluates a polynomial \( p \in R[X] \) at a fixed element \( x \in R \). Specifically, it maps each polynomial \( p \) to its evaluation \( p(x) \), preserving the ring structure: 1. \( \text{evalRingHom}(x)(1) = 1 \) 2. \( \text{evalRingHom}(x)(p \cdot q) = \text{evalRingHom}(x)(p) \cdot \text{evalRingHom}(x)(q) \) for any \( p, q \in R[X] \) 3. \( \text{evalRingHom}(x)(p + q) = \text{evalRingHom}(x)(p) + \text{evalRingHom}(x)(q) \) for any \( p, q \in R[X] \) 4. \( \text{evalRingHom}(x)(0) = 0 \)
Polynomial.coe_evalRingHom theorem
(r : R) : (evalRingHom r : R[X] → R) = eval r
Full source 
@[simp]
theorem coe_evalRingHom (r : R) : (evalRingHom r : R[X] → R) = eval r :=
  rfl
Evaluation Ring Homomorphism Coincides with Polynomial Evaluation
Informal description
For any element $r \in R$, the underlying function of the evaluation ring homomorphism $\text{evalRingHom}(r) : R[X] \to R$ coincides with the polynomial evaluation function $\text{eval}(r)$, i.e., $\text{evalRingHom}(r)(p) = p(r)$ for all $p \in R[X]$.
Polynomial.eval_pow theorem
(n : ℕ) : (p ^ n).eval x = p.eval x ^ n
Full source 
@[simp]
theorem eval_pow (n : ℕ) : (p ^ n).eval x = p.eval x ^ n :=
  eval₂_pow _ _ _
Power Law for Polynomial Evaluation: $(p^n)(x) = (p(x))^n$
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$, any element $x \in R$, and any natural number $n$, the evaluation of $p^n$ at $x$ equals the $n$-th power of the evaluation of $p$ at $x$, i.e., $$(p^n)(x) = (p(x))^n.$$
Polynomial.eval_comp theorem
: (p.comp q).eval x = p.eval (q.eval x)
Full source 
@[simp]
theorem eval_comp : (p.comp q).eval x = p.eval (q.eval x) := by
  induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs]
  | monomial n a => simp
Composition-Evaluation Commutativity: $(p \circ q)(x) = p(q(x))$
Informal description
For any polynomials $p, q \in R[X]$ and any element $x \in R$, the evaluation of the composition $p \circ q$ at $x$ equals the evaluation of $p$ at the evaluation of $q$ at $x$, i.e., $$(p \circ q)(x) = p(q(x)).$$
Polynomial.isRoot_comp theorem
{R} [CommSemiring R] {p q : R[X]} {r : R} : (p.comp q).IsRoot r ↔ p.IsRoot (q.eval r)
Full source 
lemma isRoot_comp {R} [CommSemiring R] {p q : R[X]} {r : R} :
    (p.comp q).IsRoot r ↔ p.IsRoot (q.eval r) := by simp_rw [IsRoot, eval_comp]
Root of Composition Equivalence: $(p \circ q)(r) = 0 \iff p(q(r)) = 0$
Informal description
Let $R$ be a commutative semiring, $p, q \in R[X]$ be polynomials, and $r \in R$ be an element. Then $r$ is a root of the composition $p \circ q$ if and only if $q(r)$ is a root of $p$. In other words: $$(p \circ q)(r) = 0 \iff p(q(r)) = 0.$$
Polynomial.compRingHom definition
: R[X] → R[X] →+* R[X]
Full source 
/-- `comp p`, regarded as a ring homomorphism from `R[X]` to itself. -/
def compRingHom : R[X] → R[X]R[X] →+* R[X] :=
  eval₂RingHom C
Ring homomorphism of polynomial composition with a fixed polynomial
Informal description
The function `compRingHom` maps a polynomial \( q \in R[X] \) to the ring homomorphism \( \text{comp}(\cdot, q) : R[X] \to R[X] \), which composes any polynomial \( p \in R[X] \) with \( q \) (i.e., evaluates \( p \) at \( q \)). This is a ring homomorphism, meaning it preserves addition, multiplication, and the multiplicative identity: - \( \text{comp}(p_1 + p_2, q) = \text{comp}(p_1, q) + \text{comp}(p_2, q) \) - \( \text{comp}(p_1 \cdot p_2, q) = \text{comp}(p_1, q) \cdot \text{comp}(p_2, q) \) - \( \text{comp}(1, q) = 1 \).
Polynomial.coe_compRingHom theorem
(q : R[X]) : (compRingHom q : R[X] → R[X]) = fun p => comp p q
Full source 
@[simp]
theorem coe_compRingHom (q : R[X]) : (compRingHom q : R[X] → R[X]) = fun p => comp p q :=
  rfl
Coefficient Function of Composition Ring Homomorphism is Polynomial Composition
Informal description
For any polynomial $q \in R[X]$, the underlying function of the ring homomorphism $\text{compRingHom}(q) : R[X] \to R[X]$ is given by composition with $q$, i.e., $p \mapsto p \circ q$.
Polynomial.coe_compRingHom_apply theorem
(p q : R[X]) : (compRingHom q : R[X] → R[X]) p = comp p q
Full source 
theorem coe_compRingHom_apply (p q : R[X]) : (compRingHom q : R[X] → R[X]) p = comp p q :=
  rfl
Ring Homomorphism Application for Polynomial Composition: $\text{compRingHom}(q)(p) = p \circ q$
Informal description
For any polynomials $p, q \in R[X]$, the ring homomorphism $\text{compRingHom}(q)$ applied to $p$ equals the composition $p \circ q$ of the polynomials $p$ and $q$.
Polynomial.root_mul_left_of_isRoot theorem
(p : R[X]) {q : R[X]} : IsRoot q a → IsRoot (p * q) a
Full source 
theorem root_mul_left_of_isRoot (p : R[X]) {q : R[X]} : IsRoot q a → IsRoot (p * q) a := fun H => by
  rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]
Root Preservation under Left Multiplication: $q(a) = 0 \Rightarrow (p \cdot q)(a) = 0$
Informal description
For any polynomial $p \in R[X]$ and a polynomial $q \in R[X]$, if $a \in R$ is a root of $q$ (i.e., $q(a) = 0$), then $a$ is also a root of the product $p \cdot q$ (i.e., $(p \cdot q)(a) = 0$).
Polynomial.root_mul_right_of_isRoot theorem
{p : R[X]} (q : R[X]) : IsRoot p a → IsRoot (p * q) a
Full source 
theorem root_mul_right_of_isRoot {p : R[X]} (q : R[X]) : IsRoot p a → IsRoot (p * q) a := fun H =>
  by rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]
Root Preservation under Right Multiplication: $p(a) = 0 \Rightarrow (p \cdot q)(a) = 0$
Informal description
For any polynomials $p, q \in R[X]$ and any element $a \in R$, if $a$ is a root of $p$ (i.e., $p(a) = 0$), then $a$ is also a root of the product $p \cdot q$.
Polynomial.eval₂_multiset_prod theorem
(s : Multiset R[X]) (x : S) : eval₂ f x s.prod = (s.map (eval₂ f x)).prod
Full source 
theorem eval₂_multiset_prod (s : Multiset R[X]) (x : S) :
    eval₂ f x s.prod = (s.map (eval₂ f x)).prod :=
  map_multiset_prod (eval₂RingHom f x) s
Evaluation of Polynomial Product via Ring Homomorphism: $\text{eval}_2(f, x)(\prod p) = \prod \text{eval}_2(f, x)(p)$
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $x \in S$. For any multiset $s$ of polynomials in $R[X]$, the evaluation of the product of $s$ at $x$ via $f$ equals the product of the evaluations of each polynomial in $s$ at $x$ via $f$. That is, \[ \text{eval}_2(f, x)\left(\prod_{p \in s} p\right) = \prod_{p \in s} \text{eval}_2(f, x)(p). \]
Polynomial.eval₂_finset_prod theorem
(s : Finset ι) (g : ι → R[X]) (x : S) : (∏ i ∈ s, g i).eval₂ f x = ∏ i ∈ s, (g i).eval₂ f x
Full source 
theorem eval₂_finset_prod (s : Finset ι) (g : ι → R[X]) (x : S) :
    (∏ i ∈ s, g i).eval₂ f x = ∏ i ∈ s, (g i).eval₂ f x :=
  map_prod (eval₂RingHom f x) _ _
Evaluation of Product Polynomial via Ring Homomorphism Equals Product of Evaluations
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, and $x \in S$. For any finite set $s$ and any family of polynomials $(g_i)_{i \in s}$ in $R[X]$, the evaluation of the product polynomial $\prod_{i \in s} g_i$ at $x$ via $f$ equals the product of the evaluations of each $g_i$ at $x$ via $f$. That is, \[ \text{eval}_2(f, x)\left(\prod_{i \in s} g_i\right) = \prod_{i \in s} \text{eval}_2(f, x)(g_i). \]
Polynomial.eval_list_prod theorem
(l : List R[X]) (x : R) : eval x l.prod = (l.map (eval x)).prod
Full source 
/-- Polynomial evaluation commutes with `List.prod`
-/
theorem eval_list_prod (l : List R[X]) (x : R) : eval x l.prod = (l.map (eval x)).prod :=
  map_list_prod (evalRingHom x) l
Evaluation of Polynomial Product Equals Product of Evaluations
Informal description
Let $R$ be a commutative semiring and let $l$ be a list of polynomials in $R[X]$. For any element $x \in R$, the evaluation of the product of the polynomials in $l$ at $x$ is equal to the product of the evaluations of each polynomial in $l$ at $x$. That is, \[ \text{eval}_x\left(\prod_{p \in l} p\right) = \prod_{p \in l} \text{eval}_x(p). \]
Polynomial.eval_multiset_prod theorem
(s : Multiset R[X]) (x : R) : eval x s.prod = (s.map (eval x)).prod
Full source 
/-- Polynomial evaluation commutes with `Multiset.prod`
-/
theorem eval_multiset_prod (s : Multiset R[X]) (x : R) : eval x s.prod = (s.map (eval x)).prod :=
  (evalRingHom x).map_multiset_prod s
Evaluation Commutes with Multiset Product: $\text{eval}_x(\prod p) = \prod \text{eval}_x(p)$
Informal description
Let $R$ be a commutative semiring and let $s$ be a multiset of polynomials in $R[X]$. For any element $x \in R$, the evaluation of the product of all polynomials in $s$ at $x$ equals the product of the evaluations of each polynomial in $s$ at $x$. That is, \[ \text{eval}_x \left(\prod_{p \in s} p\right) = \prod_{p \in s} \text{eval}_x(p). \]
Polynomial.eval_prod theorem
{ι : Type*} (s : Finset ι) (p : ι → R[X]) (x : R) : eval x (∏ j ∈ s, p j) = ∏ j ∈ s, eval x (p j)
Full source 
/-- Polynomial evaluation commutes with `Finset.prod`
-/
theorem eval_prod {ι : Type*} (s : Finset ι) (p : ι → R[X]) (x : R) :
    eval x (∏ j ∈ s, p j) = ∏ j ∈ s, eval x (p j) :=
  map_prod (evalRingHom x) _ _
Evaluation of Polynomial Product Equals Product of Evaluations
Informal description
Let $R$ be a commutative semiring, $\iota$ a type, $s$ a finite subset of $\iota$, and $p : \iota \to R[X]$ a family of polynomials. For any $x \in R$, the evaluation of the product of polynomials $\prod_{j \in s} p_j$ at $x$ equals the product of the evaluations of each polynomial $p_j$ at $x$: \[ \text{eval}_x \left( \prod_{j \in s} p_j \right) = \prod_{j \in s} \text{eval}_x (p_j). \]
Polynomial.list_prod_comp theorem
(l : List R[X]) (q : R[X]) : l.prod.comp q = (l.map fun p : R[X] => p.comp q).prod
Full source 
theorem list_prod_comp (l : List R[X]) (q : R[X]) :
    l.prod.comp q = (l.map fun p : R[X] => p.comp q).prod :=
  map_list_prod (compRingHom q) _
Composition Distributes Over List Product of Polynomials
Informal description
For any list $l$ of polynomials in $R[X]$ and any polynomial $q \in R[X]$, the composition of the product of $l$ with $q$ is equal to the product of the list obtained by composing each polynomial in $l$ with $q$. That is, \[ \left(\prod_{p \in l} p\right) \circ q = \prod_{p \in l} (p \circ q). \]
Polynomial.multiset_prod_comp theorem
(s : Multiset R[X]) (q : R[X]) : s.prod.comp q = (s.map fun p : R[X] => p.comp q).prod
Full source 
theorem multiset_prod_comp (s : Multiset R[X]) (q : R[X]) :
    s.prod.comp q = (s.map fun p : R[X] => p.comp q).prod :=
  map_multiset_prod (compRingHom q) _
Composition of Polynomial Product with Fixed Polynomial
Informal description
Let $R$ be a commutative semiring and let $s$ be a multiset of polynomials in $R[X]$. For any polynomial $q \in R[X]$, the composition of the product of polynomials in $s$ with $q$ is equal to the product of the compositions of each polynomial in $s$ with $q$. That is, \[ \left(\prod_{p \in s} p\right) \circ q = \prod_{p \in s} (p \circ q). \]
Polynomial.prod_comp theorem
{ι : Type*} (s : Finset ι) (p : ι → R[X]) (q : R[X]) : (∏ j ∈ s, p j).comp q = ∏ j ∈ s, (p j).comp q
Full source 
theorem prod_comp {ι : Type*} (s : Finset ι) (p : ι → R[X]) (q : R[X]) :
    (∏ j ∈ s, p j).comp q = ∏ j ∈ s, (p j).comp q :=
  map_prod (compRingHom q) _ _
Composition Distributes over Finite Product of Polynomials
Informal description
Let $R$ be a commutative semiring and let $\{p_j\}_{j \in \iota}$ be a family of polynomials in $R[X]$ indexed by a finite set $s \subseteq \iota$. For any polynomial $q \in R[X]$, the composition of the product $\prod_{j \in s} p_j$ with $q$ equals the product of the compositions of each $p_j$ with $q$, i.e., \[ \left(\prod_{j \in s} p_j\right) \circ q = \prod_{j \in s} (p_j \circ q). \]
Polynomial.isRoot_prod theorem
{R} [CommSemiring R] [IsDomain R] {ι : Type*} (s : Finset ι) (p : ι → R[X]) (x : R) : IsRoot (∏ j ∈ s, p j) x ↔ ∃ i ∈ s, IsRoot (p i) x
Full source 
theorem isRoot_prod {R} [CommSemiring R] [IsDomain R] {ι : Type*} (s : Finset ι) (p : ι → R[X])
    (x : R) : IsRootIsRoot (∏ j ∈ s, p j) x ↔ ∃ i ∈ s, IsRoot (p i) x := by
  simp only [IsRoot, eval_prod, Finset.prod_eq_zero_iff]
Root of Product of Polynomials is Root of a Factor
Informal description
Let $R$ be a commutative semiring that is also a domain, $\iota$ a type, $s$ a finite subset of $\iota$, and $p : \iota \to R[X]$ a family of polynomials. For any $x \in R$, the following are equivalent: 1. $x$ is a root of the product polynomial $\prod_{j \in s} p_j$. 2. There exists an index $i \in s$ such that $x$ is a root of $p_i$. In other words, \[ \left(\prod_{j \in s} p_j\right)(x) = 0 \iff \exists i \in s, p_i(x) = 0. \]
Polynomial.eval_dvd theorem
: p ∣ q → eval x p ∣ eval x q
Full source 
theorem eval_dvd : p ∣ q → evaleval x p ∣ eval x q :=
  eval₂_dvd _ _
Divisibility Preservation Under Polynomial Evaluation
Informal description
For any polynomials $p, q \in R[X]$ over a commutative semiring $R$ and any element $x \in R$, if $p$ divides $q$ in $R[X]$, then the evaluation of $p$ at $x$ divides the evaluation of $q$ at $x$ in $R$.
Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero theorem
: p ∣ q → eval x p = 0 → eval x q = 0
Full source 
theorem eval_eq_zero_of_dvd_of_eval_eq_zero : p ∣ q → eval x p = 0 → eval x q = 0 :=
  eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _
Root Preservation Under Divisibility in Polynomial Evaluation
Informal description
For any polynomials $p, q \in R[X]$ over a commutative semiring $R$ and any element $x \in R$, if $p$ divides $q$ and the evaluation of $p$ at $x$ is zero, then the evaluation of $q$ at $x$ is also zero. In other words, if $p \mid q$ and $p(x) = 0$, then $q(x) = 0$.
Polynomial.eval_geom_sum theorem
{R} [CommSemiring R] {n : ℕ} {x : R} : eval x (∑ i ∈ range n, X ^ i) = ∑ i ∈ range n, x ^ i
Full source 
@[simp]
theorem eval_geom_sum {R} [CommSemiring R] {n : ℕ} {x : R} :
    eval x (∑ i ∈ range n, X ^ i) = ∑ i ∈ range n, x ^ i := by simp [eval_finset_sum]
Evaluation of Geometric Sum Polynomial: $(\sum_{i=0}^{n-1} X^i)(x) = \sum_{i=0}^{n-1} x^i$
Informal description
Let $R$ be a commutative semiring, $n$ a natural number, and $x \in R$. The evaluation of the geometric sum polynomial $\sum_{i=0}^{n-1} X^i$ at $x$ equals the geometric sum $\sum_{i=0}^{n-1} x^i$. That is, $$\left(\sum_{i=0}^{n-1} X^i\right)(x) = \sum_{i=0}^{n-1} x^i.$$
Polynomial.root_mul theorem
: IsRoot (p * q) a ↔ IsRoot p a ∨ IsRoot q a
Full source 
lemma root_mul : IsRootIsRoot (p * q) a ↔ IsRoot p a ∨ IsRoot q a := by
  simp_rw [IsRoot, eval_mul, mul_eq_zero]
Roots of Product Polynomial: $(p \cdot q)(a) = 0 \leftrightarrow p(a) = 0 \lor q(a) = 0$
Informal description
For any polynomials $p, q \in R[X]$ and any element $a \in R$, the element $a$ is a root of the product $p \cdot q$ if and only if $a$ is a root of $p$ or $a$ is a root of $q$. In other words, $$(p \cdot q)(a) = 0 \leftrightarrow p(a) = 0 \lor q(a) = 0.$$
Polynomial.root_or_root_of_root_mul theorem
(h : IsRoot (p * q) a) : IsRoot p a ∨ IsRoot q a
Full source 
lemma root_or_root_of_root_mul (h : IsRoot (p * q) a) : IsRootIsRoot p a ∨ IsRoot q a :=
  root_mul.1 h
Root of Product Implies Root of a Factor
Informal description
For any polynomials $p, q \in R[X]$ and any element $a \in R$, if $a$ is a root of the product $p \cdot q$, then $a$ is a root of $p$ or $a$ is a root of $q$. In other words, if $(p \cdot q)(a) = 0$, then $p(a) = 0$ or $q(a) = 0$.
Polynomial.map_multiset_prod theorem
(m : Multiset R[X]) : m.prod.map f = (m.map <| map f).prod
Full source 
protected theorem map_multiset_prod (m : Multiset R[X]) : m.prod.map f = (m.map <| map f).prod :=
  Eq.symm <| Multiset.prod_hom _ (mapRingHom f).toMonoidHom
Ring Homomorphism Preserves Multiset Product of Polynomials
Informal description
Let $R$ and $S$ be commutative semirings, and let $f : R \to S$ be a ring homomorphism. For any multiset $m$ of polynomials in $R[X]$, the image under $f$ of the product of $m$ equals the product of the images of the polynomials in $m$ under $f$. That is, \[ f\left(\prod_{p \in m} p\right) = \prod_{p \in m} f(p). \]
Polynomial.map_prod theorem
{ι : Type*} (g : ι → R[X]) (s : Finset ι) : (∏ i ∈ s, g i).map f = ∏ i ∈ s, (g i).map f
Full source 
protected theorem map_prod {ι : Type*} (g : ι → R[X]) (s : Finset ι) :
    (∏ i ∈ s, g i).map f = ∏ i ∈ s, (g i).map f :=
  map_prod (mapRingHom f) _ _
Ring Homomorphism Commutes with Finite Product of Polynomials
Informal description
Let $R$ and $S$ be semirings, $f : R \to S$ a ring homomorphism, $\iota$ a type, $g : \iota \to R[X]$ a family of polynomials, and $s$ a finite subset of $\iota$. Then the image under $f$ of the product of polynomials $\prod_{i \in s} g(i)$ equals the product of the images: \[ \text{map}\, f \left( \prod_{i \in s} g(i) \right) = \prod_{i \in s} \text{map}\, f\, (g(i)). \]
Polynomial.map_sub theorem
{S} [Ring S] (f : R →+* S) : (p - q).map f = p.map f - q.map f
Full source 
@[simp]
protected theorem map_sub {S} [Ring S] (f : R →+* S) : (p - q).map f = p.map f - q.map f :=
  (mapRingHom f).map_sub p q
Polynomial Coefficient Mapping Preserves Subtraction
Informal description
Let $R$ and $S$ be rings, and let $f \colon R \to S$ be a ring homomorphism. For any polynomials $p, q \in R[X]$, the image of their difference under the coefficient mapping $f$ equals the difference of their images, i.e., $$(p - q).\text{map}\, f = p.\text{map}\, f - q.\text{map}\, f.$$
Polynomial.map_neg theorem
{S} [Ring S] (f : R →+* S) : (-p).map f = -p.map f
Full source 
@[simp]
protected theorem map_neg {S} [Ring S] (f : R →+* S) : (-p).map f = -p.map f :=
  (mapRingHom f).map_neg p
Negation Preservation under Polynomial Coefficient Mapping
Informal description
Let $R$ and $S$ be rings, and let $f \colon R \to S$ be a ring homomorphism. For any polynomial $p \in R[X]$, the image of $-p$ under the coefficient mapping is equal to the negation of the image of $p$, i.e., $f(-p) = -f(p)$.
Polynomial.map_intCast theorem
{S} [Ring S] (f : R →+* S) (n : ℤ) : map f ↑n = ↑n
Full source 
@[simp] protected lemma map_intCast {S} [Ring S] (f : R →+* S) (n : ℤ) : map f ↑n = ↑n :=
  map_intCast (mapRingHom f) n
Coefficient Mapping Preserves Integer Constants: $\text{map}\, f\, n = n$
Informal description
Let $R$ and $S$ be rings and $f : R \to S$ a ring homomorphism. For any integer $n \in \mathbb{Z}$, the image of the constant polynomial $n$ under the coefficient mapping $f$ is equal to the constant polynomial $n$ in $S[X]$, i.e., $\text{map}\, f\, n = n$.
Polynomial.eval_intCast theorem
{n : ℤ} {x : R} : (n : R[X]).eval x = n
Full source 
@[simp]
theorem eval_intCast {n : ℤ} {x : R} : (n : R[X]).eval x = n := by
  simp only [← C_eq_intCast, eval_C]
Evaluation of Integer Constant Polynomial: $(n)(x) = n$
Informal description
For any integer $n \in \mathbb{Z}$ and any element $x \in R$ of a semiring $R$, the evaluation of the constant polynomial $n$ in $R[X]$ at $x$ is equal to $n$ itself, i.e., $(n : R[X]).\text{eval}(x) = n$.
Polynomial.eval₂_neg theorem
{S} [Ring S] (f : R →+* S) {x : S} : (-p).eval₂ f x = -p.eval₂ f x
Full source 
@[simp]
theorem eval₂_neg {S} [Ring S] (f : R →+* S) {x : S} : (-p).eval₂ f x = -p.eval₂ f x := by
  rw [eq_neg_iff_add_eq_zero, ← eval₂_add, neg_add_cancel, eval₂_zero]
Negation Preserves Polynomial Evaluation via Ring Homomorphism: $\text{eval}_2(f, x, -p) = -\text{eval}_2(f, x, p)$
Informal description
Let $R$ and $S$ be rings, $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$ equals the negation of the evaluation of $p$ at $x$ via $f$, i.e., \[ \text{eval}_2(f, x, -p) = -\text{eval}_2(f, x, p). \]
Polynomial.eval₂_sub theorem
{S} [Ring S] (f : R →+* S) {x : S} : (p - q).eval₂ f x = p.eval₂ f x - q.eval₂ f x
Full source 
@[simp]
theorem eval₂_sub {S} [Ring S] (f : R →+* S) {x : S} :
    (p - q).eval₂ f x = p.eval₂ f x - q.eval₂ f x := by
  rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]
Subtraction Preserves Polynomial Evaluation via Ring Homomorphism: $\text{eval}_2(f, x, p - q) = \text{eval}_2(f, x, p) - \text{eval}_2(f, x, q)$
Informal description
Let $R$ and $S$ be rings, $f : R \to S$ a ring homomorphism, $p, q \in R[X]$ polynomials, and $x \in S$. Then the evaluation of $p - q$ at $x$ via $f$ equals the difference of the evaluations of $p$ and $q$ at $x$ via $f$, i.e., \[ \text{eval}_2(f, x, p - q) = \text{eval}_2(f, x, p) - \text{eval}_2(f, x, q). \]
Polynomial.eval_neg theorem
(p : R[X]) (x : R) : (-p).eval x = -p.eval x
Full source 
@[simp]
theorem eval_neg (p : R[X]) (x : R) : (-p).eval x = -p.eval x :=
  eval₂_neg _
Negation Preserves Polynomial Evaluation: $(-p)(x) = -p(x)$
Informal description
For any polynomial $p \in R[X]$ and any element $x \in R$, the evaluation of $-p$ at $x$ equals the negation of the evaluation of $p$ at $x$, i.e., \[ (-p)(x) = -p(x). \]
Polynomial.eval_sub theorem
(p q : R[X]) (x : R) : (p - q).eval x = p.eval x - q.eval x
Full source 
@[simp]
theorem eval_sub (p q : R[X]) (x : R) : (p - q).eval x = p.eval x - q.eval x :=
  eval₂_sub _
Evaluation Preserves Subtraction: $(p - q)(x) = p(x) - q(x)$
Informal description
For any polynomials $p, q \in R[X]$ and any element $x \in R$, the evaluation of the difference $p - q$ at $x$ equals the difference of the evaluations of $p$ and $q$ at $x$, i.e., \[ (p - q)(x) = p(x) - q(x). \]
Polynomial.neg_comp theorem
: (-p).comp q = -p.comp q
Full source 
@[simp]
theorem neg_comp : (-p).comp q = -p.comp q :=
  eval₂_neg _
Negation Commutes with Polynomial Composition: $(-p) \circ q = - (p \circ q)$
Informal description
For any polynomials $p, q \in R[X]$, the composition of the negation of $p$ with $q$ equals the negation of the composition of $p$ with $q$, i.e., \[ (-p) \circ q = - (p \circ q). \]
Polynomial.sub_comp theorem
: (p - q).comp r = p.comp r - q.comp r
Full source 
@[simp]
theorem sub_comp : (p - q).comp r = p.comp r - q.comp r :=
  eval₂_sub _
Composition Preserves Polynomial Subtraction: $(p - q) \circ r = p \circ r - q \circ r$
Informal description
For any polynomials $p, q, r \in R[X]$, the composition of the difference $p - q$ with $r$ equals the difference of the compositions of $p$ and $q$ with $r$, i.e., $$(p - q) \circ r = (p \circ r) - (q \circ r).$$
Polynomial.intCast_comp theorem
(i : ℤ) : comp (i : R[X]) p = i
Full source 
@[simp]
theorem intCast_comp (i : ℤ) : comp (i : R[X]) p = i := by cases i <;> simp
Composition of Integer Constant Polynomial: $(i) \circ p = i$
Informal description
For any integer $i \in \mathbb{Z}$ and any polynomial $p \in R[X]$, the composition of the constant polynomial $i$ with $p$ equals $i$ itself, i.e., $$(i : R[X]) \circ p = i.$$
Polynomial.eval₂_at_intCast theorem
{S : Type*} [Ring S] (f : R →+* S) (n : ℤ) : p.eval₂ f n = f (p.eval n)
Full source 
@[simp]
theorem eval₂_at_intCast {S : Type*} [Ring S] (f : R →+* S) (n : ℤ) :
    p.eval₂ f n = f (p.eval n) := by
  convert eval₂_at_apply (p := p) f n
  simp
Evaluation of Polynomial at Integer via Ring Homomorphism: $\text{eval}_2(f, n, p) = f(p(n))$
Informal description
Let $R$ and $S$ be rings, $f : R \to S$ a ring homomorphism, $p \in R[X]$ a polynomial, and $n \in \mathbb{Z}$ an integer. Then evaluating $p$ at $n$ via $f$ equals $f$ applied to evaluating $p$ at $n$, i.e., \[ \text{eval}_2(f, n, p) = f(\text{eval}(n, p)). \]
Polynomial.mul_X_sub_intCast_comp theorem
{n : ℕ} : (p * (X - (n : R[X]))).comp q = p.comp q * (q - n)
Full source 
theorem mul_X_sub_intCast_comp {n : ℕ} :
    (p * (X - (n : R[X]))).comp q = p.comp q * (q - n) := by
  rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]
Composition of Polynomial Product with Shifted Variable: $(p \cdot (X - n)) \circ q = (p \circ q) \cdot (q - n)$
Informal description
For any natural number $n$ and polynomials $p, q \in R[X]$, the composition of the product $p \cdot (X - n)$ with $q$ equals the product of the composition $p \circ q$ and $(q - n)$, i.e., $$(p \cdot (X - n)) \circ q = (p \circ q) \cdot (q - n).$$