evalEval_dvd

Mathlib.Algebra.Polynomial.Bivariate

URI: https://scilib.ai/kg/mathlib#Polynomial.evalEval_dvd

English

If p divides q in R[X][Y], then p.evalEval x y divides q.evalEval x y in R.

Русский

Если p делится на q в R[X][Y], то p.evalEval x y делится на q.evalEval x y в R.

LaTeX

$$$ p \\mid q \\Rightarrow p.evalEval\\ x\\ y \\mid q.evalEval\\ x\\ y $$$

Lean4

theorem evalEval_dvd (x y : R) {p q : R[X][Y]} : p ∣ q → p.evalEval x y ∣ q.evalEval x y :=
  eval_dvd ∘ eval_dvd

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru