unitLattice — Mathlib

English

The lattice formed by the image of the logarithmic embedding is the image of logEmbedding on ℤ-linear combinations of units in logSpace(K).

Русский

Латтис единиц — это образ логарифмического вложения в виде целочисленного модуля над logSpace(K).

LaTeX

$$$\mathrm{unitLattice}(K) = \mathrm{Im}(\logEmbedding K) \subseteq \logSpace(K)$$$

Lean4

/-- The lattice formed by the image of the logarithmic embedding. -/
noncomputable def _root_.NumberField.Units.unitLattice : Submodule ℤ (logSpace K) :=
  Submodule.map (logEmbedding K).toIntLinearMap ⊤

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