integerSet — Mathlib

English

An element a lies in the integer set if and only if it lies in the fundamental cone and is the image of some algebraic integer under mixedEmbedding.

Русский

Элемент a принадлежит integerSet тогда и только тогда, когда он лежит в фундаментальном конусе и является образом некоторого алгебраического целого через смешанное вложение.

LaTeX

$$a \in integerSet(K) \iff a \in fundamentalCone(K) \land (\exists x: 𝓞K, mixedEmbedding(K) x = a).$$

Lean4

/-- The intersection between the fundamental cone and the `integerLattice`. -/
def integerSet : Set (mixedSpace K) :=
  fundamentalCone K ∩ mixedEmbedding.integerLattice K

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