normAtAllPlaces_eq_of_normAtComplexPlaces_eq

English

If two mixed-space elements have the same norm at complex places, then they have the same norm at all places.

Русский

Если у двух элементов смешанного пространства одна и та же норма на комплексных местах, то на всех местах нормы равны.

LaTeX

$$$$\text{If } \operatorname{normAtComplexPlaces}(x) = \operatorname{normAtComplexPlaces}(y) \text{ then } \operatorname{normAtAllPlaces}(x) = \operatorname{normAtAllPlaces}(y).$$$$

Lean4

theorem normAtAllPlaces_eq_of_normAtComplexPlaces_eq {x y : mixedSpace K}
    (h : normAtComplexPlaces x = normAtComplexPlaces y) : normAtAllPlaces x = normAtAllPlaces y :=
  by
  ext w
  obtain hw | hw := isReal_or_isComplex w
  ·
    simpa [normAtAllPlaces_apply, normAtPlace_apply_of_isReal hw, normAtComplexPlaces_apply_isReal ⟨w, hw⟩] using
      congr_arg (|·|) (congr_fun h w)
  ·
    simpa [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw, normAtComplexPlaces_apply_isComplex ⟨w, hw⟩] using
      congr_fun h w

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