mkComplex — Mathlib

English

Outline: mkReal provides a bijection between real embeddings and real infinite places by sending φ to mk φ and vice versa.

Русский

Набросок: mkReal задаёт биекцию между реальными вложениями и реальными бесконечными местами, отображая φ ↦ mk φ и наоборот.

LaTeX

$$mkReal : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : \mathrm{InfinitePlace}(K) // IsReal w }$$

Lean4

/-- The map from nonreal embeddings to complex infinite places -/
noncomputable def mkComplex : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } → { w : InfinitePlace K // IsComplex w } :=
  Subtype.map mk fun φ hφ => ⟨φ, hφ, rfl⟩

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