normAtPlace_apply_of_isReal — Mathlib

English

For a real place w, normAtPlace w x equals the real-part norm of x at w's embedding: normAtPlace w x = || x_1(⟨w, hw⟩) ||.

Русский

Для вещественного места w норма-At-Place равна норме вещественной части вложения x в w: normAtPlace w x = || x_1(⟨w, hw⟩) ||.

LaTeX

$$$\operatorname{normAtPlace}(w)(x) = \lVert x_1(\langle w, hw \rangle) \rVert.$$$

Lean4

theorem normAtPlace_apply_of_isReal {w : InfinitePlace K} (hw : IsReal w) (x : mixedSpace K) :
    normAtPlace w x = ‖x.1 ⟨w, hw⟩‖ := by rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dif_pos]

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