isRoot_root — Mathlib

English

The root f is a root of the polynomial f mapped along the natural map from R[X] to AdjoinRoot f; i.e., root f is a root of f.map(of f).

Русский

Корень f является корнем полинома f, отображенного через естественную карту из R[X] в AdjoinRoot f.

LaTeX

$$$\\mathrm{IsRoot}(f.map(\\mathrm{of}\\, f), \\mathrm{root}(f))$$$

Lean4

theorem isRoot_root (f : R[X]) : IsRoot (f.map (of f)) (root f) := by rw [IsRoot, eval_map, eval₂_root]

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