eval₂_derivative_ne_zero — Mathlib

English

Let f: R →+* S be a ring homomorphism and p ∈ R[X] be separable. If p(x) = 0 for some x ∈ S, then the derivative of p evaluated at x is nonzero.

Русский

Пусть f: R →+* S — гомоморфизм колец и p ∈ R[X] раздельный. Если существует x ∈ S такое, что p(x) = 0, то p'(x) ≠ 0.

LaTeX

$$$\\operatorname{Separable}(p) \\Rightarrow \\forall x,\\ p(x)=0 \\Rightarrow (p')(x) \\neq 0$$$

Lean4

theorem eval₂_derivative_ne_zero [Nontrivial S] (f : R →+* S) {p : R[X]} (h : p.Separable) {x : S}
    (hx : p.eval₂ f x = 0) : (derivative p).eval₂ f x ≠ 0 :=
  by
  intro hx'
  obtain ⟨a, b, e⟩ := h
  apply_fun Polynomial.eval₂ f x at e
  simp only [eval₂_add, eval₂_mul, hx, mul_zero, hx', add_zero, eval₂_one, zero_ne_one] at e

Похожие утверждения