integerLattice — Mathlib

English

The image of the ring of integers 𝓞_K in the Euclidean mixed space is described as a Z-lattice via the mixed embedding.

Русский

Образ кольца целых 𝓞_K в евклидовом смешаном пространстве задаётся как Z-решетка через смешанное вложение.

LaTeX

$$Image(\mathcal{O}_K) in (euclidean.mixedSpace K) equals Z-lattice via (toMixed K).$$

Lean4

/-- The image of ring of integers `𝓞 K` in the Euclidean mixed space. -/
protected def integerLattice : Submodule ℤ (euclidean.mixedSpace K) :=
  ZLattice.comap ℝ (mixedEmbedding.integerLattice K) (toMixed K).toLinearMap

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