normAtComplexPlaces_apply_isReal — Mathlib

English

normAtComplexPlaces_apply_isReal: for w real, normAtComplexPlaces x w = x.1 w.

Русский

Для действительного места w, норма на комплексном наборе совпадает с исходной нормой.

LaTeX

$$$\forall {x : mixedSpace K} \; (w : { w // IsReal w}),\n\; \text{normAtComplexPlaces } x w = x.1 w.$$$

Lean4

@[simp]
theorem normAtComplexPlaces_apply_isReal {x : mixedSpace K} (w : { w // IsReal w }) : normAtComplexPlaces x w = x.1 w :=
  by rw [normAtComplexPlaces, dif_pos]

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