mem_roots_map_of_injective — Mathlib

English

For nonzero p, x is a root of p iff aeval x p = 0.

Русский

Для ненулевого p корень x следует из aeval x p = 0.

LaTeX

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

Lean4

theorem mem_roots_map_of_injective [Semiring S] {p : S[X]} {f : S →+* R} (hf : Function.Injective f) {x : R}
    (hp : p ≠ 0) : x ∈ (p.map f).roots ↔ p.eval₂ f x = 0 := by
  rw [mem_roots ((Polynomial.map_ne_zero_iff hf).mpr hp), IsRoot, eval_map]

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