aeval_derivative_ne_zero — Mathlib

English

Let f: R →+* S be a RingHom and p ∈ R[X] be separable. If aeval x p = 0 for some x in S, then aeval x (derivative p) ≠ 0.

Русский

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

LaTeX

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

Lean4

theorem aeval_derivative_ne_zero [Nontrivial S] [Algebra R S] {p : R[X]} (h : p.Separable) {x : S}
    (hx : aeval x p = 0) : aeval x (derivative p) ≠ 0 :=
  h.eval₂_derivative_ne_zero (algebraMap R S) hx

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