primPart_ne_zero

Mathlib.RingTheory.Polynomial.Content

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

English

The primitive part of any nonzero polynomial is nonzero.

Русский

Примитивная часть любого ненулевого многочлена ненулевая.

LaTeX

$$$p.primPart \neq 0$$$

Lean4

theorem primPart_ne_zero (p : R[X]) : p.primPart ≠ 0 :=
  p.isPrimitive_primPart.ne_zero

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

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

Разделы

Аффилиация

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