IsReal — Mathlib

English

An infinite place w is real if there exists a real embedding φ such that mk φ = w.

Русский

Бесконечное место w над K является реальным, если существует реальное вложение φ такое, что mk φ = w.

LaTeX

$$$IsReal(w) \iff \\exists \\varphi : K \\\\to+* \\\\mathbb{C}, \\\\text{ComplexEmbedding.IsReal} \\\\varphi \. \\\\wedge \\\\mathrm{mk} \\\\varphi = w.$$$

Lean4

/-- An infinite place is real if it is defined by a real embedding. -/
def IsReal (w : InfinitePlace K) : Prop :=
  ∃ φ : K →+* ℂ, ComplexEmbedding.IsReal φ ∧ mk φ = w

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