commMap_apply_of_isReal — Mathlib

English

The real-span of the canonical lattice basis and the kernel of commMap are disjoint subspaces.

Русский

Образы вещественного подпространства базисной решётки канонического отображения и ядро commMap не пересекаются.

LaTeX

$$$\mathrm{Disjoint}\Big( \mathrm{span}_{\mathbb{R}}(\mathrm{range}(\mathrm{canonicalEmbedding}.\mathrm{latticeBasis}(K))), \ker(\mathrm{commMap}(K)) \Big).$$$

Lean4

theorem commMap_apply_of_isReal (x : (K →+* ℂ) → ℂ) {w : InfinitePlace K} (hw : IsReal w) :
    (commMap K x).1 ⟨w, hw⟩ = (x w.embedding).re :=
  rfl

Похожие утверждения