logEmbedding — Mathlib

English

The logarithmic embedding is a homomorphism from the additive group of units to logSpace.

Русский

Логарифмическое вложение является гомоморфизмом от аддитивной группы единиц к logSpace.

LaTeX

$$$\logEmbedding : \mathrm{Units}(\mathcal{O}_K) \to \logSpace(K)$$$

Lean4

/-- The logarithmic embedding of the units (seen as an `Additive` group). -/
def _root_.NumberField.Units.logEmbedding : Additive ((𝓞 K)ˣ) →+ logSpace K :=
  { toFun := fun x w ↦ mult w.val * Real.log (w.val ↑x.toMul)
    map_zero' := by simp; rfl
    map_add' := fun _ _ ↦ by simp [Real.log_mul, mul_add]; rfl }

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