Theorems · Definition · number theory

NumberField.mixedEmbedding.latticeBasis

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Module.Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℝ
        (NumberField.mixedEmbedding.mixedSpace K)

A ℝ-basis of the mixed space that is also a ℤ-basis of the image of 𝓞 K.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

FieldNumberField