normAtAllPlaces_norm_at_real_places

English

Norms at complex places coincide with the global norm after embedding into the real space.

Русский

Нормы на комплексных местах совпадают с глобальной нормой после встраивания в реальное пространство.

LaTeX

$$$$\operatorname{normAtComplexPlaces}(\operatorname{mixedSpaceOfRealSpace}(\operatorname{normAtAllPlaces}(x))) = \operatorname{normAtAllPlaces}(x).$$$$

Lean4

theorem normAtAllPlaces_norm_at_real_places (x : mixedSpace K) :
    normAtAllPlaces (fun w ↦ ‖x.1 w‖, x.2) = normAtAllPlaces x :=
  by
  ext w
  obtain hw | hw := isReal_or_isComplex w
  · simp_rw [normAtAllPlaces, normAtPlace_apply_of_isReal hw, norm_norm]
  · simp_rw [normAtAllPlaces, normAtPlace_apply_of_isComplex hw]

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