mixedSpaceOfRealSpace — Mathlib

English

The map from realSpace K to mixedSpace K is the natural embedding that acts as identity on real places and sends real values to complex places via inclusion.

Русский

Естественное вложение: realSpace K → mixedSpace K, сохраняющее вещественные места и переводя вещественные значения в комплексные через включение.

LaTeX

$$mixedSpaceOfRealSpace : realSpace(K) →L[ℝ] mixedSpace(K)$$

Lean4

/-- The continuous linear map from `realSpace K` to `mixedSpace K` which is the identity at real
places and the natural map `ℝ → ℂ` at complex places.
-/
def mixedSpaceOfRealSpace : realSpace K →L[ℝ] mixedSpace K :=
  .prod (.pi fun w ↦ .proj w.1) (.pi fun w ↦ Complex.ofRealCLM.comp (.proj w.1))

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