Theorems · Definition · number theory

NumberField.mixedEmbedding.fundamentalCone.completeBasis

(K : Type u_1) →
  [inst : Field K] →
    [NumberField K] → Module.Basis (NumberField.InfinitePlace K) ℝ (NumberField.mixedEmbedding.realSpace K)

A basis of realSpace K formed by the image of the fundamental units (which form a basis of a subspace {x : realSpace K | ∑ w, x w = 0}) and the vector (mult w)_w. For i ≠ w₀, the image of completeBasis K i by the natural restriction map realSpace K → logSpace K is basisUnitLattice K

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Cited by

16 results in Mathlib

Foundations

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

Assumes

FieldNumberField