IsComplex — Mathlib

English

An infinite place w is complex if it is defined by a non-real (complex) embedding.

Русский

Бесконечное место w над K является комплексным, если оно задаётся не реальным, а комплексным вложением.

LaTeX

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

Lean4

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

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