eval_gcd_eq_zero — Mathlib

English

For polynomials f and g and a ring hom, if f and g evaluate to zero at α, then eval of gcd vanishes at α.

Русский

Для многочленов f, g и кольцевого гомоморфа, если f(α)=0 и g(α)=0, тогда gcd(f,g)(α)=0.

LaTeX

$$$ \operatorname{eval}_\phi^\alpha(\gcd f g) = 0 $ given $ \operatorname{eval}_\phi^\alpha f = 0$ and $ \operatorname{eval}_\phi^\alpha g = 0 $$$

Lean4

theorem eval_gcd_eq_zero [DecidableEq R] {f g : R[X]} {α : R} (hf : f.eval α = 0) (hg : g.eval α = 0) :
    (EuclideanDomain.gcd f g).eval α = 0 :=
  eval₂_gcd_eq_zero hf hg

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