primPart_dvd

Mathlib.RingTheory.Polynomial.Content

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

English

The primitive part of p divides p.

Русский

Примитивная часть p делит p.

LaTeX

$$$p.primPart \mid p$$$

Lean4

theorem primPart_dvd (p : R[X]) : p.primPart ∣ p :=
  Dvd.intro_left (C p.content) p.eq_C_content_mul_primPart.symm

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

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

Разделы

Аффилиация

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