isPrimitive_one

Mathlib.RingTheory.Polynomial.Content

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

English

The constant polynomial 1 is primitive in the polynomial ring over any commutative ring.

Русский

Константный полином 1 примитивен в кольце полиномов над любой коммутативной областью.

LaTeX

$$$$ \\text{IsPrimitive}(1) $$$$

Lean4

@[simp]
theorem isPrimitive_one : IsPrimitive (1 : R[X]) := fun _ h => isUnit_C.mp (isUnit_of_dvd_one h)

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

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

Разделы

Аффилиация

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