cyclotomic_zero

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

← MathLib Explorer

English

The zeroth cyclotomic polynomial is the constant polynomial 1.

Русский

Нулевой циклотоми́ческий полином равен константе 1.

LaTeX

$$$\operatorname{cyclotomic}(0,R) = 1$$$

Lean4

/-- The zeroth cyclotomic polynomial is `1`. -/
@[simp]
theorem cyclotomic_zero (R : Type*) [Ring R] : cyclotomic 0 R = 1 := by simp only [cyclotomic, dif_pos]

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

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

Разделы

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

Аффилиация

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