eval_nodal_not_at_node — Mathlib

English

No common root among the x value and the nodes implies nonvanishing evaluation.

Русский

Если x не совпадает ни с одним узлом v(i), i∈s, и в кольце нет нулевых делителей, то eval_x nodal(s,v) ≠ 0.

LaTeX

$$$ [\\text{NoZeroDivisors }R] \\Rightarrow (\\forall x)(\\forall s,v)(\\forall hx, \\forall i\\in s, x \\neq v(i) ) \\Rightarrow \\operatorname{eval}_x(\\operatorname{nodal}(s,v)) \\neq 0. $$$

Lean4

theorem eval_nodal_not_at_node [Nontrivial R] [NoZeroDivisors R] {x : R} (hx : ∀ i ∈ s, x ≠ v i) :
    eval x (nodal s v) ≠ 0 :=
  by
  simp_rw [nodal, eval_prod, prod_ne_zero_iff, eval_sub, eval_X, eval_C, sub_ne_zero]
  exact hx

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