normAtPlace_negAt — Mathlib

English

NegAt preserves the placewise norm: for x, ||(negAt s x)_{w}|| = ||x_{w}|| for all places w.

Русский

NegAt сохраняет норму по месту: для всех локальных составляющих нормa не изменяется.

LaTeX

$$normAtPlace_negAt (x) w = normAtPlace x w$$

Lean4

/-- `negAt` preserves `normAtPlace`. -/
@[simp]
theorem normAtPlace_negAt (x : mixedSpace K) (w : InfinitePlace K) : normAtPlace w (negAt s x) = normAtPlace w x :=
  by
  obtain hw | hw := isReal_or_isComplex w
  · simp_rw [normAtPlace_apply_of_isReal hw, negAt_apply_norm_isReal]
  · simp_rw [normAtPlace_apply_of_isComplex hw, negAt_apply_isComplex]

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