expMapBasis_nonneg

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.fundamentalCone.expMapBasis_nonneg

English

For any x and any infinite place w, 0 < expMapBasis x w.

Русский

Для любых x и бесконечных мест w выполняется 0 < expMapBasis x w.

LaTeX

$$$\forall x\in\mathbb{R}^{r},\ \forall w\in \text{InfinitePlace},\ 0<\expMapBasis(x)(w)$$$

Lean4

theorem expMapBasis_nonneg (x : realSpace K) (w : InfinitePlace K) : 0 ≤ expMapBasis x w :=
  (expMapBasis_pos _ _).le

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

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

Разделы

Аффилиация

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