eta_sq_add_eta_add_one

Mathlib.NumberTheory.Cyclotomic.Three

URI: https://scilib.ai/kg/mathlib#IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one

English

For any x in the ring of integers, λ divides x, or x−1, or x+1.

Русский

Для любого x в кольце целых λ делит x, или x−1, или x+1.

LaTeX

$$$\lambda \mid x \; \text{или}\; \lambda \mid (x-1) \; \text{или}\; \lambda \mid (x+1)$$$

Lean4

/-- We have that `η ^ 2 + η + 1 = 0`. -/
theorem eta_sq_add_eta_add_one : (η : 𝓞 K) ^ 2 + η + 1 = 0 :=
  by
  rw [eta_sq]
  ring

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

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

Разделы

Аффилиация

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