mk_conjugate_eq — Mathlib

English

Taking complex conjugation of the embedding yields the same infinite place after applying mk.

Русский

Сложение по комплексному сопряжению вложения даёт то же самое бесконечное место после применения mk.

LaTeX

$$mk (ComplexEmbedding.conjugate φ) = mk φ$$

Lean4

@[simp]
theorem mk_conjugate_eq (φ : K →+* ℂ) : mk (ComplexEmbedding.conjugate φ) = mk φ :=
  by
  refine DFunLike.ext _ _ (fun x => ?_)
  rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.norm_conj]

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