normAtPlace_mixedSpaceOfRealSpace

English

normAtComplexPlaces_apply_isReal: for a real place w, normAtComplexPlaces x w = x w.

Русский

Для действительного места w нормa AtComplexPlaces совпадает с исходной нормой на этом месте.

LaTeX

$$$\forall \; x:\, mixedSpace K, \ w: { w // IsReal w},\n\; \text{normAtComplexPlaces } x w = x.1 w.$$$

Lean4

theorem normAtPlace_mixedSpaceOfRealSpace {x : realSpace K} {w : InfinitePlace K} (hx : 0 ≤ x w) :
    normAtPlace w (mixedSpaceOfRealSpace x) = x w :=
  by
  simp only [mixedSpaceOfRealSpace_apply]
  obtain hw | hw := isReal_or_isComplex w
  · rw [normAtPlace_apply_of_isReal hw, Real.norm_of_nonneg hx]
  · rw [normAtPlace_apply_of_isComplex hw, Complex.norm_of_nonneg hx]

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