norm_normAtAllPlaces — Mathlib

English

For every x in the mixed space, the mixedEmbedding norm is preserved after applying normAtAllPlaces to x and taking the real-space representation: mixedEmbedding.norm(mixedSpaceOfRealSpace(normAtAllPlaces x)) = mixedEmbedding.norm x.

Русский

Для каждого x в смешанном пространстве нормировка через normAtAllPlaces сохраняет норму: mixedEmbedding.norm(mixedSpaceOfRealSpace(normAtAllPlaces x)) = mixedEmbedding.norm x.

LaTeX

$$$\\operatorname{mixedEmbedding.norm}\\bigl(\\operatorname{mixedSpaceOfRealSpace}(\\operatorname{normAtAllPlaces} x)\\bigr) = \\operatorname{mixedEmbedding.norm} x$$$

Lean4

theorem norm_normAtAllPlaces (x : mixedSpace K) :
    mixedEmbedding.norm (mixedSpaceOfRealSpace (normAtAllPlaces x)) = mixedEmbedding.norm x := by
  simp_rw [mixedEmbedding.norm_apply, normAtPlace_mixedSpaceOfRealSpace (normAtAllPlaces_nonneg _ _)]

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