mem_roots_iff_aeval_eq_zero — Mathlib

English

∀ {R} [Domain], {p : Polynomial R} {x}, (p ≠ 0) → x ∈ roots p ↔ aeval x p = 0

Русский

∀ R, домен, p ∈ R[X], x, p ≠ 0 → x ∈ roots p ↔ aeval x p = 0

LaTeX

$$∀ {R} [IsDomain R] {p : Polynomial R} {x : R}, p ≠ 0 → (x ∈ p.roots ↔ aeval x p = 0).$$

Lean4

theorem mem_roots_iff_aeval_eq_zero {x : R} (w : p ≠ 0) : x ∈ roots p ↔ aeval x p = 0 := by
  rw [aeval_def, ← mem_roots_map_of_injective (FaithfulSMul.algebraMap_injective _ _) w, Algebra.algebraMap_self,
    map_id]

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