mem_roots_map — Mathlib

English

For p ≠ 0, x is a root of p.map f exactly when p.eval₂ f x = 0.

Русский

Пусть p ≠ 0. Тогда x является корнем p.map f тогда и только тогда, когда p.eval₂ f x = 0.

LaTeX

$$$ x \in (p.map f).\mathrm{roots} \iff p.eval_2 f x = 0 \quad (p \neq 0) $$$

Lean4

theorem mem_roots_map [CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) :
    x ∈ (p.map f).roots ↔ p.eval₂ f x = 0 := by rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]

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