Theorems · Definition · number theory

NumberField.mixedEmbedding.stdBasis

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

The ℝ-basis of the mixed space of K formed by the vector equal to 1 at w and 0 elsewhere for IsReal w and by the couple of vectors equal to 1 (resp. I) at w and 0 elsewhere for IsComplex w.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

FieldNumberField