normAtPlace_polarCoord_symm_of_isReal

English

For every x in the real part of the mixed space and every real place w, the place-norm of the inverse polar coordinate equals the real coordinate at w.

Русский

Для каждого x в реальной части смешанного пространства и каждого вещественного места w нормa места для $(\\mathrm{polarCoord})^{-1}x$ равна норме соответствующей компоненты x на w.

LaTeX

$$$\\forall x \\in \\text{realMixedSpace}(K), \\forall w\\, (hw : \\ IsReal\, w), \\\\ \\| \\operatorname{normAtPlace}(w)((\\mathrm{polarCoord}(K)).\\mathrm{symm}x) \\| = \\| x.1 \\langle w, hw \\rangle \\|$$

Lean4

theorem normAtPlace_polarCoord_symm_of_isReal (x : realMixedSpace K) {w : InfinitePlace K} (hw : IsReal w) :
    normAtPlace w ((mixedEmbedding.polarCoord K).symm x) = ‖x.1 ⟨w, hw⟩‖ := by simp [normAtPlace_apply_of_isReal hw]

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