negAt — Mathlib

English

The map negAt is its own inverse.

Русский

Отображение negAt является собственным обратным.

LaTeX

$$negAt s is its own inverse: (negAt s)^{-1} = negAt s.$$

Lean4

/-- Let `s` be a set of real places, define the continuous linear equiv of the mixed space that
swaps sign at places in `s` and leaves the rest unchanged. -/
def negAt : mixedSpace K ≃L[ℝ] mixedSpace K :=
  (piCongrRight fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prodCongr
    (ContinuousLinearEquiv.refl ℝ _)

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