normAtPlace_apply — Mathlib

English

In general, normAtPlace w x equals the appropriate coordinate's norm (real or complex) depending on w.

Русский

В общем случае норма на месте совпадает с нормой соответствующей координаты (вещественной или комплексной) в зависимости от w.

LaTeX

$$$\operatorname{normAtPlace}(w)(x) = \begin{cases} \|x_1(\langle w, hw \rangle)\|, & \text{if } w \text{ real}, \\ \|x_2(\langle w, hw \rangle)\|, & \text{if } w \text{ complex}. \end{cases}$$$

Lean4

@[simp]
theorem normAtPlace_apply (w : InfinitePlace K) (x : K) : normAtPlace w (mixedEmbedding K x) = w x := by
  simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply,
    norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite, ite_id]

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