Mathlib.Algebra.Polynomial.Eval.Coeff

Polynomial.eval₂_at_zero theorem

: p.eval₂ f 0 = f (coeff p 0)

Full source

@[simp]
theorem eval₂_at_zero : p.eval₂ f 0 = f (coeff p 0) := by
  simp +contextual only [eval₂_eq_sum, zero_pow_eq, mul_ite, mul_zero,
    mul_one, sum, Classical.not_not, mem_support_iff, sum_ite_eq', ite_eq_left_iff,
    RingHom.map_zero, imp_true_iff, eq_self_iff_true]

Evaluation at Zero via Ring Homomorphism: $\text{eval}_2(f, p, 0) = f(p_0)$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$ and any ring homomorphism $f : R \to S$ to another semiring $S$, the evaluation of $p$ at $0$ under $f$ equals $f$ applied to the constant term of $p$, i.e., $$ \text{eval}_2(f, p, 0) = f(p_0) $$ where $p_0$ is the coefficient of $X^0$ in $p$.

Polynomial.eval₂_C_X theorem

: eval₂ C X p = p

Full source

@[simp]
theorem eval₂_C_X : eval₂ C X p = p :=
  Polynomial.induction_on' p (fun p q hp hq => by simp [hp, hq]) fun n x => by
    rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']

Evaluation Identity: $\text{eval}_2(C, X, p) = p$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, the evaluation of $p$ at $X$ using the constant polynomial homomorphism $C$ as the coefficient map is equal to $p$ itself. In other words, evaluating $p$ by treating its coefficients as constant polynomials and $X$ as the polynomial variable returns the original polynomial: $$\text{eval}_2(C, X, p) = p.$$

Polynomial.coeff_zero_eq_eval_zero theorem

(p : R[X]) : coeff p 0 = p.eval 0

Full source

theorem coeff_zero_eq_eval_zero (p : R[X]) : coeff p 0 = p.eval 0 :=
  calc
    coeff p 0 = coeff p 0 * 0 ^ 0 := by simp
    _ = p.eval 0 := by
      symm
      rw [eval_eq_sum]
      exact Finset.sum_eq_single _ (fun b _ hb => by simp [zero_pow hb]) (by simp)

Constant Term Equals Evaluation at Zero: $p(0) = a_0$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, the coefficient of the constant term $X^0$ in $p$ is equal to the evaluation of $p$ at $0$, i.e., $p(0) = a_0$ where $a_0$ is the coefficient of $X^0$ in $p$.

Polynomial.zero_isRoot_of_coeff_zero_eq_zero theorem

{p : R[X]} (hp : p.coeff 0 = 0) : IsRoot p 0

Full source

theorem zero_isRoot_of_coeff_zero_eq_zero {p : R[X]} (hp : p.coeff 0 = 0) : IsRoot p 0 := by
  rwa [coeff_zero_eq_eval_zero] at hp

Zero Root Condition: $a_0 = 0 \Rightarrow p(0) = 0$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, if the constant term coefficient $a_0$ (i.e., the coefficient of $X^0$) is zero, then $0$ is a root of $p$, meaning $p(0) = 0$.

Polynomial.coeff_map theorem

(n : ℕ) : coeff (p.map f) n = f (coeff p n)

Full source

@[simp]
theorem coeff_map (n : ℕ) : coeff (p.map f) n = f (coeff p n) := by
  rw [map, eval₂_def, coeff_sum, sum]
  conv_rhs => rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]
  refine Finset.sum_congr rfl fun x _hx => ?_
  simp only [RingHom.coe_comp, Function.comp, coeff_C_mul_X_pow]
  split_ifs <;> simp [f.map_zero]

Coefficient Preservation under Polynomial Map: $\text{coeff}(f(p), n) = f(\text{coeff}(p, n))$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, any ring homomorphism $f \colon R \to S$ to another semiring $S$, and any natural number $n$, the coefficient of $X^n$ in the polynomial $f(p)$ obtained by applying $f$ to each coefficient of $p$ is equal to $f$ applied to the coefficient of $X^n$ in $p$. In other words: $$\text{coeff}(f(p), n) = f(\text{coeff}(p, n))$$

Polynomial.coeff_map_eq_comp theorem

(p : R[X]) (f : R →+* S) : (p.map f).coeff = f ∘ p.coeff

Full source

lemma coeff_map_eq_comp (p : R[X]) (f : R →+* S) : (p.map f).coeff = f ∘ p.coeff := by
  ext n; exact coeff_map ..

Coefficient Function Composition under Polynomial Map: $(f \circ p)_n = f(p_n)$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$ and any ring homomorphism $f \colon R \to S$ to another semiring $S$, the coefficient function of the mapped polynomial $f(p)$ is equal to the composition of $f$ with the coefficient function of $p$. That is, for all $n \in \mathbb{N}$, $$(f(p))_n = f(p_n).$$

Polynomial.map_map theorem

[Semiring T] (g : S →+* T) (p : R[X]) : (p.map f).map g = p.map (g.comp f)

Full source

theorem map_map [Semiring T] (g : S →+* T) (p : R[X]) : (p.map f).map g = p.map (g.comp f) :=
  ext (by simp [coeff_map])

Composition of Polynomial Maps: $g(f(p)) = (g \circ f)(p)$

Informal description

Let $R$, $S$, and $T$ be semirings, and let $f \colon R \to S$ and $g \colon S \to T$ be ring homomorphisms. For any polynomial $p \in R[X]$, the composition of polynomial maps satisfies: $$g(f(p)) = (g \circ f)(p)$$ where $f(p)$ denotes the polynomial obtained by applying $f$ to each coefficient of $p$, and similarly for $g(f(p))$.

Polynomial.map_id theorem

: p.map (RingHom.id _) = p

Full source

@[simp]
theorem map_id : p.map (RingHom.id _) = p := by simp [Polynomial.ext_iff, coeff_map]

Identity Mapping Preserves Polynomial: $\text{id}(p) = p$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, the polynomial obtained by applying the identity ring homomorphism to each coefficient of $p$ is equal to $p$ itself.

Polynomial.piEquiv definition

{ι} [Finite ι] (R : ι → Type*) [∀ i, Semiring (R i)] : (∀ i, R i)[X] ≃+* ∀ i, (R i)[X]

Full source

/-- The polynomial ring over a finite product of rings is isomorphic to
the product of polynomial rings over individual rings. -/
def piEquiv {ι} [Finite ι] (R : ι → Type*) [∀ i, Semiring (R i)] :
    (∀ i, R i)[X](∀ i, R i)[X] ≃+* ∀ i, (R i)[X] :=
  .ofBijective (Pi.ringHom fun i ↦ mapRingHom (Pi.evalRingHom R i))
    ⟨fun p q h ↦ by ext n i; simpa using congr_arg (fun p ↦ coeff (p i) n) h,
      fun p ↦ ⟨.ofFinsupp (.ofSupportFinite (fun n i ↦ coeff (p i) n) <|
        (Set.finite_iUnion fun i ↦ (p i).support.finite_toSet).subset fun n hn ↦ by
          simp only [Set.mem_iUnion, Finset.mem_coe, mem_support_iff, Function.mem_support] at hn ⊢
          contrapose! hn; exact funext hn), by ext i n; exact coeff_map _ _⟩⟩

Polynomial ring isomorphism for product of semirings

Informal description

For a finite index set $\iota$ and a family of semirings $(R_i)_{i \in \iota}$, the polynomial ring over the product semiring $\prod_{i \in \iota} R_i$ is isomorphic as a ring to the product of polynomial rings $\prod_{i \in \iota} R_i[X]$. More precisely, the isomorphism is constructed by mapping a polynomial $p \in (\prod_i R_i)[X]$ to the family of polynomials $(p_i)_{i \in \iota}$ where each $p_i \in R_i[X]$ is obtained by evaluating the coefficients of $p$ at the $i$-th component.

Polynomial.map_injective theorem

(hf : Function.Injective f) : Function.Injective (map f)

Full source

theorem map_injective (hf : Function.Injective f) : Function.Injective (map f) := fun p q h =>
  ext fun m => hf <| by rw [← coeff_map f, ← coeff_map f, h]

Injectivity of Polynomial Map Induced by Injective Ring Homomorphism

Informal description

Let $R$ and $S$ be semirings and $f: R \to S$ be an injective ring homomorphism. Then the induced polynomial map $f_*: R[X] \to S[X]$, which applies $f$ to each coefficient of a polynomial, is also injective.

Polynomial.map_injective_iff theorem

: Function.Injective (map f) ↔ Function.Injective f

Full source

theorem map_injective_iff : Function.InjectiveFunction.Injective (map f) ↔ Function.Injective f :=
  ⟨fun h r r' eq ↦ by simpa using h (a₁ := C r) (a₂ := C r') (by simpa), map_injective f⟩

Injectivity of Polynomial Map vs. Ring Homomorphism Injectivity

Informal description

The polynomial map induced by a ring homomorphism $f: R \to S$ is injective if and only if $f$ itself is injective. In other words, the map $f_*: R[X] \to S[X]$ that applies $f$ to each coefficient of a polynomial is injective precisely when $f$ is injective.

Polynomial.map_surjective theorem

(hf : Function.Surjective f) : Function.Surjective (map f)

Full source

theorem map_surjective (hf : Function.Surjective f) : Function.Surjective (map f) := fun p =>
  p.induction_on'
    (by rintro _ _ ⟨p, rfl⟩ ⟨q, rfl⟩; exact ⟨p + q, Polynomial.map_add f⟩)
    fun n s ↦
    let ⟨r, hr⟩ := hf s
    ⟨monomial n r, by rw [map_monomial f, hr]⟩

Surjectivity of Polynomial Map Induced by Surjective Ring Homomorphism

Informal description

Let $R$ and $S$ be semirings and $f: R \to S$ be a surjective ring homomorphism. Then the induced polynomial map $f_*: R[X] \to S[X]$, which applies $f$ to each coefficient of a polynomial, is also surjective.

Polynomial.map_surjective_iff theorem

: Function.Surjective (map f) ↔ Function.Surjective f

Full source

theorem map_surjective_iff : Function.SurjectiveFunction.Surjective (map f) ↔ Function.Surjective f :=
  ⟨fun h s ↦ let ⟨p, h⟩ := h (C s); ⟨p.coeff 0, by simpa using congr(coeff $h 0)⟩, map_surjective f⟩

Surjectivity of Polynomial Map Equivalence: $f_*$ is surjective $\leftrightarrow$ $f$ is surjective

Informal description

For any ring homomorphism $f \colon R \to S$ between semirings, the induced polynomial map $f_* \colon R[X] \to S[X]$ is surjective if and only if $f$ is surjective.

Polynomial.map_eq_zero_iff theorem

(hf : Function.Injective f) : p.map f = 0 ↔ p = 0

Full source

protected theorem map_eq_zero_iff (hf : Function.Injective f) : p.map f = 0 ↔ p = 0 :=
  map_eq_zero_iff (mapRingHom f) (map_injective f hf)

Injective Ring Homomorphism Preserves Nonzero Polynomials

Informal description

Let $R$ and $S$ be semirings and $f: R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, the polynomial obtained by applying $f$ to each coefficient of $p$ is the zero polynomial in $S[X]$ if and only if $p$ is the zero polynomial in $R[X]$. In other words, $f_*(p) = 0$ if and only if $p = 0$.

Polynomial.map_ne_zero_iff theorem

(hf : Function.Injective f) : p.map f ≠ 0 ↔ p ≠ 0

Full source

protected theorem map_ne_zero_iff (hf : Function.Injective f) : p.map f ≠ 0p.map f ≠ 0 ↔ p ≠ 0 :=
  (Polynomial.map_eq_zero_iff hf).not

Injective Ring Homomorphism Preserves Nonzero Polynomials: $f_*(p) \neq 0 \leftrightarrow p \neq 0$

Informal description

Let $R$ and $S$ be semirings and $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, the polynomial obtained by applying $f$ to each coefficient of $p$ is nonzero in $S[X]$ if and only if $p$ is nonzero in $R[X]$. In other words, $f_*(p) \neq 0$ if and only if $p \neq 0$.

Polynomial.mapRingHom_id theorem

: mapRingHom (RingHom.id R) = RingHom.id R[X]

Full source

@[simp]
theorem mapRingHom_id : mapRingHom (RingHom.id R) = RingHom.id R[X] :=
  RingHom.ext fun _x => map_id

Identity Polynomial Ring Homomorphism: $\text{mapRingHom}(\text{id}_R) = \text{id}_{R[X]}$

Informal description

The polynomial ring homomorphism induced by the identity ring homomorphism on a semiring $R$ is equal to the identity ring homomorphism on the polynomial ring $R[X]$. In other words, the map $\text{mapRingHom}(\text{id}_R) = \text{id}_{R[X]}$ holds.

Polynomial.mapRingHom_comp theorem

[Semiring T] (f : S →+* T) (g : R →+* S) : (mapRingHom f).comp (mapRingHom g) = mapRingHom (f.comp g)

Full source

@[simp]
theorem mapRingHom_comp [Semiring T] (f : S →+* T) (g : R →+* S) :
    (mapRingHom f).comp (mapRingHom g) = mapRingHom (f.comp g) :=
  RingHom.ext <| Polynomial.map_map g f

Composition of Polynomial Map Homomorphisms: $(\text{mapRingHom}\, f) \circ (\text{mapRingHom}\, g) = \text{mapRingHom}\, (f \circ g)$

Informal description

Let $R$, $S$, and $T$ be semirings, and let $f \colon S \to T$ and $g \colon R \to S$ be ring homomorphisms. Then the composition of the polynomial map homomorphisms satisfies: $$(\text{mapRingHom}\, f) \circ (\text{mapRingHom}\, g) = \text{mapRingHom}\, (f \circ g)$$ where $\text{mapRingHom}\, f$ denotes the ring homomorphism that applies $f$ to each coefficient of a polynomial, and $\circ$ denotes composition of ring homomorphisms.

Polynomial.eval₂_map theorem

[Semiring T] (g : S →+* T) (x : T) : (p.map f).eval₂ g x = p.eval₂ (g.comp f) x

Full source

theorem eval₂_map [Semiring T] (g : S →+* T) (x : T) :
    (p.map f).eval₂ g x = p.eval₂ (g.comp f) x := by
  rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]

Evaluation of Mapped Polynomial via Composition of Homomorphisms: $(f(p))(g, x) = p(g \circ f, x)$

Informal description

Let $R$, $S$, and $T$ be semirings, and let $f \colon R \to S$ and $g \colon S \to T$ be ring homomorphisms. For any polynomial $p \in R[X]$ and any element $x \in T$, the evaluation of the mapped polynomial $p.map(f)$ under the evaluation homomorphism $g$ at $x$ is equal to the evaluation of $p$ under the composed homomorphism $g \circ f$ at $x$. That is, $$(p.map(f)).eval₂(g, x) = p.eval₂(g \circ f, x).$$

Polynomial.eval_zero_map theorem

(f : R →+* S) (p : R[X]) : (p.map f).eval 0 = f (p.eval 0)

Full source

@[simp]
theorem eval_zero_map (f : R →+* S) (p : R[X]) : (p.map f).eval 0 = f (p.eval 0) := by
  simp [← coeff_zero_eq_eval_zero]

Evaluation of Mapped Polynomial at Zero: $(f(p))(0) = f(p(0))$

Informal description

For any ring homomorphism $f \colon R \to S$ between semirings and any polynomial $p \in R[X]$, evaluating the mapped polynomial $f(p)$ at $0$ is equal to $f$ applied to the evaluation of $p$ at $0$, i.e., $$(f(p))(0) = f(p(0)).$$

Polynomial.eval_one_map theorem

(f : R →+* S) (p : R[X]) : (p.map f).eval 1 = f (p.eval 1)

Full source

@[simp]
theorem eval_one_map (f : R →+* S) (p : R[X]) : (p.map f).eval 1 = f (p.eval 1) := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
  | monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]

Evaluation of Mapped Polynomial at One: $(f(p))(1) = f(p(1))$

Informal description

For any ring homomorphism $f \colon R \to S$ between semirings and any polynomial $p \in R[X]$, evaluating the mapped polynomial $f(p)$ at $1$ is equal to $f$ applied to the evaluation of $p$ at $1$, i.e., $$(f(p))(1) = f(p(1)).$$

Polynomial.eval_natCast_map theorem

(f : R →+* S) (p : R[X]) (n : ℕ) : (p.map f).eval (n : S) = f (p.eval n)

Full source

@[simp]
theorem eval_natCast_map (f : R →+* S) (p : R[X]) (n : ℕ) :
    (p.map f).eval (n : S) = f (p.eval n) := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
  | monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]

Evaluation of Mapped Polynomial at Natural Number: $(f(p))(n) = f(p(n))$

Informal description

For any ring homomorphism $f \colon R \to S$ between semirings, any polynomial $p \in R[X]$, and any natural number $n$, the evaluation of the mapped polynomial $f(p)$ at $n$ (viewed as an element of $S$) equals $f$ applied to the evaluation of $p$ at $n$, i.e., $$(f(p))(n) = f(p(n)).$$

Polynomial.eval_intCast_map theorem

{R S : Type*} [Ring R] [Ring S] (f : R →+* S) (p : R[X]) (i : ℤ) : (p.map f).eval (i : S) = f (p.eval i)

Full source

@[simp]
theorem eval_intCast_map {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (p : R[X]) (i : ℤ) :
    (p.map f).eval (i : S) = f (p.eval i) := by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
  | monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]

Evaluation of Mapped Polynomial at Integer: $(p.map\,f)(i) = f(p(i))$

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]$ and any integer $i \in \mathbb{Z}$, the evaluation of the mapped polynomial $p.map\,f$ at the integer $i$ (viewed as an element of $S$) equals the image under $f$ of the evaluation of $p$ at $i$. That is, $$(p.map\,f)(i) = f(p(i)).$$

Polynomial.hom_eval₂ theorem

(x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x)

Full source

theorem hom_eval₂ (x : S) : g (p.eval₂ f x) = p.eval₂ (g.comp f) (g x) := by
  rw [← eval₂_map, eval₂_at_apply, eval_map]

Compatibility of Polynomial Evaluation with Ring Homomorphisms: $g(p(f, x)) = p(g \circ f, g(x))$

Informal description

Let $R$, $S$, and $T$ be semirings, let $f \colon R \to S$ and $g \colon S \to T$ be ring homomorphisms, and let $p \in R[X]$ be a polynomial. For any $x \in S$, we have $$g(p.eval₂(f, x)) = p.eval₂(g \circ f, g(x)).$$

Polynomial.eval₂_hom theorem

(x : R) : p.eval₂ f (f x) = f (p.eval x)

Full source

theorem eval₂_hom (x : R) : p.eval₂ f (f x) = f (p.eval x) :=
  RingHom.comp_id f ▸ (hom_eval₂ p (RingHom.id R) f x).symm

Compatibility of Polynomial Evaluation with Ring Homomorphisms: $p(f, f(x)) = f(p(x))$

Informal description

Let $R$ and $S$ be semirings, let $f \colon R \to S$ be a ring homomorphism, and let $p \in R[X]$ be a polynomial. For any $x \in R$, the evaluation of $p$ at $f(x)$ using the homomorphism $f$ equals $f$ applied to the evaluation of $p$ at $x$, i.e., $$p.eval₂(f, f(x)) = f(p.eval(x)).$$

Polynomial.evalRingHom_zero theorem

: evalRingHom 0 = constantCoeff

Full source

theorem evalRingHom_zero : evalRingHom 0 = constantCoeff :=
  DFunLike.ext _ _ fun p => p.coeff_zero_eq_eval_zero.symm

Evaluation at Zero Equals Constant Coefficient Homomorphism

Informal description

The evaluation ring homomorphism at zero is equal to the constant coefficient ring homomorphism, i.e., $\text{evalRingHom}(0) = \text{constantCoeff}$.

Polynomial.support_map_subset theorem

[Semiring R] [Semiring S] (f : R →+* S) (p : R[X]) : (map f p).support ⊆ p.support

Full source

theorem support_map_subset [Semiring R] [Semiring S] (f : R →+* S) (p : R[X]) :
    (map f p).support ⊆ p.support := by
  intro x
  contrapose!
  simp +contextual

Support Subset Under Polynomial Map: $\text{supp}(f(p)) \subseteq \text{supp}(p)$

Informal description

Let $R$ and $S$ be semirings, $f \colon R \to S$ be a ring homomorphism, and $p \in R[X]$ be a polynomial. Then the support of the polynomial $f(p)$ is a subset of the support of $p$, i.e., $$\text{supp}(f(p)) \subseteq \text{supp}(p).$$

Polynomial.support_map_of_injective theorem

[Semiring R] [Semiring S] (p : R[X]) {f : R →+* S} (hf : Function.Injective f) : (map f p).support = p.support

Full source

theorem support_map_of_injective [Semiring R] [Semiring S] (p : R[X]) {f : R →+* S}
    (hf : Function.Injective f) : (map f p).support = p.support := by
  simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
    forall_const]

Support Preservation under Injective Polynomial Map: $\text{supp}(f(p)) = \text{supp}(p)$

Informal description

Let $R$ and $S$ be semirings, $p \in R[X]$ a polynomial, and $f \colon R \to S$ an injective ring homomorphism. Then the support of the polynomial $f(p)$ (obtained by applying $f$ to each coefficient of $p$) is equal to the support of $p$. That is: $$\text{supp}(f(p)) = \text{supp}(p)$$ where $\text{supp}(p)$ denotes the set of exponents $n$ for which the coefficient of $X^n$ in $p$ is nonzero.

Polynomial.IsRoot.map theorem

{f : R →+* S} {x : R} {p : R[X]} (h : IsRoot p x) : IsRoot (p.map f) (f x)

Full source

theorem IsRoot.map {f : R →+* S} {x : R} {p : R[X]} (h : IsRoot p x) : IsRoot (p.map f) (f x) := by
  rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]

Root Preservation under Polynomial Map: $p(x) = 0 \Rightarrow f(p)(f(x)) = 0$

Informal description

Let $R$ and $S$ be semirings, $f \colon R \to S$ be a ring homomorphism, $x \in R$, and $p \in R[X]$ be a polynomial. If $x$ is a root of $p$ (i.e., $p(x) = 0$), then $f(x)$ is a root of the polynomial $f(p)$ obtained by applying $f$ to each coefficient of $p$.

Polynomial.IsRoot.of_map theorem

{R} [Ring R] {f : R →+* S} {x : R} {p : R[X]} (h : IsRoot (p.map f) (f x)) (hf : Function.Injective f) : IsRoot p x

Full source

theorem IsRoot.of_map {R} [Ring R] {f : R →+* S} {x : R} {p : R[X]} (h : IsRoot (p.map f) (f x))
    (hf : Function.Injective f) : IsRoot p x := by
  rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]

Root Reflection under Injective Polynomial Map: $f(p)(f(x)) = 0 \Rightarrow p(x) = 0$

Informal description

Let $R$ be a ring, $S$ a semiring, $f \colon R \to S$ an injective ring homomorphism, $x \in R$, and $p \in R[X]$ a polynomial. If $f(x)$ is a root of the polynomial $p.map(f)$ (obtained by applying $f$ to each coefficient of $p$), then $x$ is a root of $p$.

Polynomial.isRoot_map_iff theorem

 {R : Type*} [CommRing R] {f : R →+* S} {x : R} {p : R[X]} (hf : Function.Injective f) :
  IsRoot (p.map f) (f x) ↔ IsRoot p x

Full source

theorem isRoot_map_iff {R : Type*} [CommRing R] {f : R →+* S} {x : R} {p : R[X]}
    (hf : Function.Injective f) : IsRootIsRoot (p.map f) (f x) ↔ IsRoot p x :=
  ⟨fun h => h.of_map hf, fun h => h.map⟩

Root Preservation and Reflection under Injective Polynomial Map: $f(p)(f(x)) = 0 \leftrightarrow p(x) = 0$

Informal description

Let $R$ be a commutative ring, $S$ a semiring, $f \colon R \to S$ an injective ring homomorphism, $x \in R$, and $p \in R[X]$ a polynomial. Then $f(x)$ is a root of the polynomial $p.map(f)$ (obtained by applying $f$ to each coefficient of $p$) if and only if $x$ is a root of $p$.