Theorems · Theorem · number theory

NumberField.mixedEmbedding.disjoint_span_commMap_ker

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Disjoint (Submodule.span ℝ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K)))
    (NumberField.mixedEmbedding.commMap K).ker

This is a technical result to ensure that the image of the ℂ-basis of ℂ^n defined in canonicalEmbedding.latticeBasis is a ℝ-basis of the mixed space ℝ^r₁ × ℂ^r₂, see mixedEmbedding.latticeBasis.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNumberField