isPrimitive

Mathlib.RingTheory.Polynomial.Content

URI: https://scilib.ai/kg/mathlib#Polynomial.Monic.isPrimitive

← MathLib Explorer

English

If a polynomial p is monic, then p is primitive.

Русский

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

LaTeX

$$$$ \\text{Monic}(p) \\Rightarrow p \\text{ is primitive} $$$$

Lean4

theorem isPrimitive {p : R[X]} (hp : p.Monic) : p.IsPrimitive :=
  by
  rintro r ⟨q, h⟩
  exact isUnit_of_mul_eq_one r (q.coeff p.natDegree) (by rwa [← coeff_C_mul, ← h])

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

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

Разделы

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

Аффилиация

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