root_gcd_iff_root_left_right — Mathlib

English

For polynomials f and g, gcd vanishes at α iff both f and g vanish at α under a ring hom.

Русский

Для многочленов f и g gcd обнуляется в α тогда и только тогда, когда оба f и g обнуляются в α при кольцевом гомоморфизме.

LaTeX

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

Lean4

theorem root_gcd_iff_root_left_right [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k} :
    (EuclideanDomain.gcd f g).eval₂ ϕ α = 0 ↔ f.eval₂ ϕ α = 0 ∧ g.eval₂ ϕ α = 0 :=
  ⟨fun h => ⟨root_left_of_root_gcd h, root_right_of_root_gcd h⟩, fun h => eval₂_gcd_eq_zero h.1 h.2⟩

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