Theorems · Definition · number theory

NumberField.mixedEmbedding.logMap

{K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.mixedEmbedding.mixedSpace K → NumberField.Units.dirichletUnitTheorem.logSpace K

The map from the mixed space to logSpace K defined in such way that: 1) it factors the map logEmbedding, see logMap_eq_logEmbedding; 2) it is constant on the sets {c • x | c ∈ ℝ, c ≠ 0} if norm x ≠ 0, see logMap_real_smul.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Cited by

21 results in Mathlib

Foundations

Depth 299 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField