isComplex_iff — Mathlib

English

IsComplex w is equivalent to not ComplexEmbedding.IsReal (embedding w).

Русский

IsComplex w эквивалентно не Real embedding (embedding w).

LaTeX

$$$IsComplex(w) \iff \\neg \\mathrm{ComplexEmbedding.IsReal}(\\mathrm{embedding}(w)).$$$

Lean4

theorem isComplex_iff {w : InfinitePlace K} : IsComplex w ↔ ¬ComplexEmbedding.IsReal (embedding w) :=
  by
  refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
  rintro ⟨φ, ⟨hφ, rfl⟩⟩
  contrapose! hφ
  cases mk_eq_iff.mp (mk_embedding (mk φ)) with
  | inl h => rwa [h] at hφ
  | inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

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