dedekindZeta_residue_ne_zero

Mathlib.NumberTheory.NumberField.DedekindZeta

URI: https://scilib.ai/kg/mathlib#NumberField.dedekindZeta_residue_ne_zero

English

The Dedekind zeta residue is nonzero: 0 ≠ dedekindZeta_residue(K).

Русский

Резидуал Dedekind zeta не равен нулю: 0 ≠ dedekindZeta_residue(K).

LaTeX

$$$\mathrm{dedekindZeta\_residue}(K) \neq 0$$$

Lean4

theorem dedekindZeta_residue_ne_zero : dedekindZeta_residue K ≠ 0 :=
  (dedekindZeta_residue_pos K).ne'

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

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

Разделы

Аффилиация

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