normAtComplexPlaces_polarSpaceCoord_symm

English

polarSpaceCoord is an OpenPartialHomeomorph between the mixed space and the polar space.

Русский

polarSpaceCoord есть открытое частичное гомеоморфное отображение между смешанным пространством и полярным пространством.

LaTeX

$$$\\text{polarSpaceCoord} : \\text{OpenPartialHomeomorph}(\\text{mixedSpace}(K), \\text{polarSpace}(K))$$$

Lean4

theorem normAtComplexPlaces_polarSpaceCoord_symm [NumberField K] (x : polarSpace K) :
    normAtComplexPlaces ((polarSpaceCoord K).symm x) = normAtComplexPlaces (mixedSpaceOfRealSpace x.1) :=
  by
  ext w
  obtain hw | hw := isReal_or_isComplex w
  · simp [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]
  · simp [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]

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