commMap_apply_of_isComplex — Mathlib

English

The norm at a place w is a monoid-with-zero hom from the mixed space to ℝ, defined coordinatewise by taking either the absolute value of the real part or the modulus of the complex part depending on whether w is real or complex.

Русский

Норма на месте w есть гомоморфизм моноидов с нулём из смешанного пространства в ℝ, задаваемый по координатам: для вещественного места берём модуль вещественной части, для комплексного — модуль комплексной части.

LaTeX

$$$\mathrm{normAtPlace}(w): (\mathrm{mixedSpace}(K)) \to_0 \mathbb{R},\quad \text{defined by } x \mapsto \begin{cases} |x_1(w)|, & \text{if } w \text{ real}; \\ |x_2(w)|, & \text{if } w \text{ complex}. \end{cases}$$$

Lean4

theorem commMap_apply_of_isComplex (x : (K →+* ℂ) → ℂ) {w : InfinitePlace K} (hw : IsComplex w) :
    (commMap K x).2 ⟨w, hw⟩ = x w.embedding :=
  rfl

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