negAt_signSet_apply_isComplex — Mathlib

English

Let x be in the mixed space and w a complex place. Then the second component at w of (negAt (signSet x) x) equals x.2 w; the complex part is unchanged by negAt on real-sign flipping. In particular, (negAt (signSet x) x).2 w = x.2 w for w with IsComplex.

Русский

Пусть x лежит в смешанном пространстве, а w — комплексное место. Тогда в месте w вторая компонента (negAt (signSet x) x) равна x.2 w; комплексная часть не меняется при negAt с учётом signSet. В частности, (negAt (signSet x) x).2 w = x.2 w при IsComplex.

LaTeX

$$$\forall x\in \text{mixedSpace}(K),\forall w:\{ w: \text{InfinitePlace}(K) \mid \text{IsComplex}(w)\},\ (negAt (signSet x) x)_2(w)=x_2(w)$$$

Lean4

@[simp]
theorem negAt_signSet_apply_isComplex (x : mixedSpace K) (w : { w // IsComplex w }) :
    (negAt (signSet x) x).2 w = x.2 w :=
  rfl

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