coe_eta

Mathlib.NumberTheory.Cyclotomic.Three

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

English

In a cubic cyclotomic setting, the element η in the ring of integers 𝓞K is equal to the integer hζ.toInteger.

Русский

В кубической циклотомической конфигурации элемент η в кольце целых 𝓞K равен целому числу hζ.toInteger.

LaTeX

$$$(\eta : \mathcal{O}_K) = h_{\zeta}.to\mathrm{Integer}$$$

Lean4

theorem coe_eta : (η : 𝓞 K) = hζ.toInteger :=
  rfl

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

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

Разделы

Аффилиация

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