w₀

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

URI: https://scilib.ai/kg/mathlib#NumberField.Units.dirichletUnitTheorem.w₀

English

There exists a distinguished infinite place w0 in InfinitePlace(K).

Русский

Существует выделенное бесконечное место w0 в InfinitePlace(K).

LaTeX

$$$w_0 \in \mathrm{InfinitePlace}(K)$ (distinguished)$$

Lean4

/-- The distinguished infinite place. -/
def w₀ : InfinitePlace K :=
  (inferInstance : Nonempty (InfinitePlace K)).some

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

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

Разделы

Аффилиация

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