eval₂_gcd_eq_zero — Mathlib

English

If f and g evaluate to zero at α under ϕ, then evaluating gcd(f,g) under ϕ at α yields zero.

Русский

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

LaTeX

$$$ \operatorname{eval}_2\; \varphi\; \alpha\; (\gcd f g) = 0 $$$

Lean4

theorem eval₂_gcd_eq_zero [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k} (hf : f.eval₂ ϕ α = 0)
    (hg : g.eval₂ ϕ α = 0) : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0 := by
  rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul, Polynomial.eval₂_mul, hf, hg,
    zero_mul, zero_mul, zero_add]

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