mem_rootSet — Mathlib

English

Membership in rootSet is equivalent to nonzero and evaluation zero.

Русский

Принадлежность к rootSet эквивалентна неравенству нулю многочлена и нулю значения p(а).

LaTeX

$$$$ a \in p.rootSet S \;\iff\; p \neq 0 \land \operatorname{aeval}(a,p) = 0 $$$$

Lean4

theorem mem_rootSet {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : S} :
    a ∈ p.rootSet S ↔ p ≠ 0 ∧ aeval a p = 0 := by
  rw [mem_rootSet', Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)]

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