C_content_dvd

Mathlib.RingTheory.Polynomial.Content

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

English

For any polynomial p in R[X], the constant polynomial with value equal to the content of p, C(content(p)), divides p.

Русский

Для любого многочлена p над кольцом R следует, что константный многочлен C(content(p)) делит p.

LaTeX

$$$C\bigl(\operatorname{content}(p)\bigr) \mid p$$$

Lean4

theorem C_content_dvd (p : R[X]) : C p.content ∣ p :=
  dvd_content_iff_C_dvd.1 dvd_rfl

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

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

Разделы

Аффилиация

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