Theorems · Definition · number theory

NumberField.canonicalEmbedding.latticeBasis

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Module.Basis (Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K)) ℂ ((K →+* ℂ) → ℂ)

A ℂ-basis of ℂ^n that is also a ℤ-basis of the integerLattice.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

FieldNumberField