Theorems · Definition · number theory

NumberField.mixedEmbedding.fundamentalCone.expMapBasis

{K : Type u_1} →
  [inst : Field K] →
    [NumberField K] →
      OpenPartialHomeomorph (NumberField.mixedEmbedding.realSpace K) (NumberField.mixedEmbedding.realSpace K)

The map that sends x : realSpace K to Real.exp (x w₀) * ∏_{i ≠ w₀} |ηᵢ| ^ x i where |ηᵢ| denote the vector of realSpace K given by w (ηᵢ) and ηᵢ denote the units in fundSystem K, see expMapBasis_apply'.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Cited by

30 results in Mathlib

Foundations

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

Assumes

FieldNumberField