Theorems · Definition · number theory

NumberField.mixedEmbedding.fractionalIdealLatticeBasis

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) →
        Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑↑I) ℝ (NumberField.mixedEmbedding.mixedSpace K)

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

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

FieldNumberField