cyclotomic_three

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

English

For any ring R, Φ_3(R) = X^2 + X + 1.

Русский

Для любого кольца R Φ_3(R) = X^2 + X + 1.

LaTeX

$$$$\mathrm{cyclotomic}\ 3\ R = X^2 + X + 1.$$$$

Lean4

@[simp]
theorem cyclotomic_three (R : Type*) [Ring R] : cyclotomic 3 R = X ^ 2 + X + 1 := by
  simp [cyclotomic_prime, sum_range_succ']

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

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

Разделы

Аффилиация

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