root_left_of_root_gcd — Mathlib

English

If gcd(f,g) vanishes at α, then f vanishes at α under ϕ.

Русский

Если gcd(f,g) обнуляется в α, то f обнуляется в α под ϕ.

LaTeX

$$$ (\gcd f g).eval_2\;\varphi\;\alpha = 0 \Rightarrow f.eval_2\;\varphi\;\alpha = 0 $$$

Lean4

theorem root_left_of_root_gcd [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k}
    (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : f.eval₂ ϕ α = 0 :=
  by
  obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_left f g
  rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

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