Mathlib.Algebra.Polynomial.Eval.Algebra

Module docstring

{"# Evaluation of polynomials in an algebra

This file concerns evaluating polynomials where the map is algebraMap

TODO: merge with parts of Algebra/Polynomial/AlgebraMap.lean? "}

Polynomial.eval₂_mul' theorem

: (p * q).eval₂ (algebraMap R S) x = p.eval₂ (algebraMap R S) x * q.eval₂ (algebraMap R S) x

Full source

@[simp]
theorem eval₂_mul' :
    (p * q).eval₂ (algebraMap R S) x = p.eval₂ (algebraMap R S) x * q.eval₂ (algebraMap R S) x := by
  exact eval₂_mul_noncomm _ _ fun k => Algebra.commute_algebraMap_left (coeff q k) x

Evaluation of Polynomial Product via Algebra Map

Informal description

Let $R$ be a commutative semiring and $S$ be a semiring with an algebra map $\text{algebraMap} : R \to S$. For any polynomials $p, q \in R[X]$ and any element $x \in S$, the evaluation of the product polynomial $p * q$ at $x$ via $\text{algebraMap}$ equals the product of the evaluations of $p$ and $q$ at $x$, i.e., $$(p * q).\text{eval}_2 (\text{algebraMap} R S) x = p.\text{eval}_2 (\text{algebraMap} R S) x \cdot q.\text{eval}_2 (\text{algebraMap} R S) x.$$

Polynomial.eval₂_pow' theorem

(n : ℕ) : (p ^ n).eval₂ (algebraMap R S) x = (p.eval₂ (algebraMap R S) x) ^ n

Full source

@[simp]
theorem eval₂_pow' (n : ℕ) :
    (p ^ n).eval₂ (algebraMap R S) x = (p.eval₂ (algebraMap R S) x) ^ n := by
  induction n with
  | zero => simp only [pow_zero, eval₂_one]
  | succ n ih => rw [pow_succ, pow_succ, eval₂_mul', ih]

Power Evaluation via Algebra Map: $(p^n)(x) = (p(x))^n$

Informal description

Let $R$ be a commutative semiring and $S$ a semiring with an algebra map $\text{algebraMap} : R \to S$. For any polynomial $p \in R[X]$, element $x \in S$, and natural number $n$, the evaluation of the polynomial $p^n$ at $x$ via $\text{algebraMap}$ equals the $n$-th power of the evaluation of $p$ at $x$, i.e., $$(p^n).\text{eval}_2 (\text{algebraMap} R S) x = (p.\text{eval}_2 (\text{algebraMap} R S) x)^n.$$

Polynomial.eval₂_comp' theorem

: eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p

Full source

@[simp]
theorem eval₂_comp' : eval₂ (algebraMap R S) x (p.comp q) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p := by
  induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
  | monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']

Evaluation of Polynomial Composition via Algebra Map

Informal description

Let $R$ be a commutative semiring and $S$ a semiring with an algebra map $\text{algebraMap} \colon R \to S$. For any polynomials $p, q \in R[X]$ and any element $x \in S$, the evaluation of the composition polynomial $p \circ q$ at $x$ via $\text{algebraMap}$ equals the evaluation of $p$ at the evaluation of $q$ at $x$, i.e., $$\text{eval}_2 (\text{algebraMap} R S) x (p \circ q) = \text{eval}_2 (\text{algebraMap} R S) (\text{eval}_2 (\text{algebraMap} R S) x q) p.$$