mixedEmbedding_apply_isComplex — Mathlib

English

For each x in K and a complex place w, the complex component of the mixed embedding is the complex embedding at w: (mixedEmbedding K x).2 w = w.val.embedding x.

Русский

Для каждого x и сложного места w вторая компонента смешанного вложения равна комплексному вложению: (mixedEmbedding K x).2 w = w.val.embedding x.

LaTeX

$$$ (\mathrm{mixedEmbedding}(K)\; x)_2(w) = w.\text{val}.embedding\ x. $$$

Lean4

@[simp]
theorem mixedEmbedding_apply_isComplex (x : K) (w : { w // IsComplex w }) :
    (mixedEmbedding K x).2 w = w.val.embedding x := by simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]

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