eval₂_dvd

Mathlib.Algebra.Polynomial.Eval.Defs

URI: https://scilib.ai/kg/mathlib#Polynomial.eval₂_dvd

English

Evaluation preserves divisibility: if p divides q in R[X], then eval₂ f x p divides eval₂ f x q in S.

Русский

Оценка сохраняет делимость: если p делит q в R[X], то eval₂ f x p делит eval₂ f x q в S.

LaTeX

$$$\text{ev}_{f,x}(p) \mid \text{ev}_{f,x}(q) \quad\text{whenever } p \mid q$$$

Lean4

@[gcongr]
theorem eval₂_dvd : p ∣ q → eval₂ f x p ∣ eval₂ f x q :=
  map_dvd (eval₂RingHom f x)

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

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

Разделы

Аффилиация

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