normAtPlace — Mathlib

English

If w is a complex place, normAtPlace at x equals the complex embedding modulus: (normAtPlace w)(x) = || x_2(w) ||.

Русский

Если w — комплексное место, то нормa на месте равна модулю комплексной части: (normAtPlace w)(x) = || x_2( w ) ||.

LaTeX

$$$\operatorname{normAtPlace}(w)(x) = \|x_2(\langle w, \mathrm{IsComplex}(w)\rangle)\|.$$$

Lean4

/-- The norm at the infinite place `w` of an element of the mixed space -/
def normAtPlace (w : InfinitePlace K) : (mixedSpace K) →*₀ ℝ
    where
  toFun x := if hw : IsReal w then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, not_isReal_iff_isComplex.mp hw⟩‖
  map_zero' := by simp
  map_one' := by simp
  map_mul' x y := by split_ifs <;> simp

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