mixedEmbedding_apply_isReal — Mathlib

English

For each x in K and a real place w, the real component of the mixed embedding coincides with the corresponding real embedding: (mixedEmbedding K x).1 w = embedding_of_isReal w.prop x.

Русский

Для каждого элемента x поля K и вещественного места w, первая компонента смешанного вложения совпадает с вещественным вложением: (mixedEmbedding K x).1 w = embedding_of_isReal w.prop x.

LaTeX

$$$ (\mathrm{mixedEmbedding}(K)\; x)_1(w) = \mathrm{embedding\_of\_isReal}(w.\text{prop})\, x. $$$

Lean4

@[simp]
theorem mixedEmbedding_apply_isReal (x : K) (w : { w // IsReal w }) :
    (mixedEmbedding K x).1 w = embedding_of_isReal w.prop x := by
  simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]

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