eval₂_dvd — Mathlib

English

If p divides q in the polynomial ring, then their images under eval₂ preserve divisibility.

Русский

Если p делит q в полиномном кольце, то их образы под eval₂ сохраняют делимость.

LaTeX

$$$\text{If } p \mid q, \; p.eval₂ f g \;|\; q.eval₂ f g$$$

Lean4

@[gcongr]
theorem eval₂_dvd (f : R →+* S₁) (g : σ → S₁) {p q : MvPolynomial σ R} (h : p ∣ q) : p.eval₂ f g ∣ q.eval₂ f g :=
  map_dvd (eval₂Hom f g) h

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