mem_rootSet_of_ne — Mathlib

English

If p ≠ 0, then a ∈ rootSet S(p) iff aeval(a) p = 0.

Русский

Если p ≠ 0, тогда a ∈ rootSet(p) в S тогда и только если p(a) = 0.

LaTeX

$$$$ p \neq 0 \Rightarrow \left( a \in p.rootSet S \iff \operatorname{aeval}(a,p) = 0 \right) $$$$

Lean4

theorem mem_rootSet_of_ne {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S]
    (hp : p ≠ 0) {a : S} : a ∈ p.rootSet S ↔ aeval a p = 0 :=
  mem_rootSet.trans <| and_iff_right hp

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