isPrimitive_of_dvd

Mathlib.RingTheory.Polynomial.Content

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

← MathLib Explorer

English

If p is primitive and q divides p, then q is primitive.

Русский

Если p примитивен и q делит p, то q примитивен.

LaTeX

$$$$ p.IsPrimitive \\rightarrow (q \\mid p) \\Rightarrow q.IsPrimitive $$$$

Lean4

theorem isPrimitive_of_dvd {p q : R[X]} (hp : IsPrimitive p) (hq : q ∣ p) : IsPrimitive q := fun a ha =>
  isPrimitive_iff_isUnit_of_C_dvd.mp hp a (dvd_trans ha hq)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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