mem_rootSet_of_injective — Mathlib

English

If the algebra map S → R is injective and p ≠ 0, then x ∈ p.rootSet R iff aeval x p = 0.

Русский

Если отображение алгебры S → R инъективно и p ≠ 0, то x ∈ p.rootSet R эквивалентно aeval x p = 0.

LaTeX

$$$$ x \in p.rootSet R \iff \mathrm{aeval}(x)\,p = 0, \quad p \neq 0 $$$$

Lean4

theorem mem_rootSet_of_injective [CommRing S] {p : S[X]} [Algebra S R] (h : Function.Injective (algebraMap S R)) {x : R}
    (hp : p ≠ 0) : x ∈ p.rootSet R ↔ aeval x p = 0 := by
  classical exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

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