root_mul_left_of_isRoot — Mathlib

English

If p ∈ R[X] and q ∈ R[X], then IsRoot p a → IsRoot (p · q) a, i.e. multiplying on the right by q preserves the root at a as long as p has a root at a.

Русский

Если p имеет корень в a, то произведение p·q имеет корень в a.

LaTeX

$$$\\text{IsRoot } p a \\rightarrow \\text{IsRoot } (p\\cdot q) a$$$

Lean4

theorem root_mul_left_of_isRoot (p : R[X]) {q : R[X]} : IsRoot q a → IsRoot (p * q) a := fun H => by
  rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]

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