conjNeg_symm — Mathlib

English

Let G and H be additive commutative groups, and a ∈ G, b ∈ H. The operation conjNeg with parameters a and b is an involutive symmetry, i.e., it is its own inverse: (conjNeg (a := a) (b := b))^{-1} = conjNeg (a := a) (b := b).

Русский

Пусть G и H — аддитивные коммутативные группы, а также a ∈ G, b ∈ H. Операция conjNeg с параметрами a и b является инволюционным симметризмом: она равна своей обратной, то есть (conjNeg (a := a) (b := b))^{-1} = conjNeg (a := a) (b := b).

LaTeX

$$$ (\operatorname{conjNeg})^{-1} = \operatorname{conjNeg} $$$

Lean4

@[simp]
theorem conjNeg_symm : (conjNeg (a := a) (b := b)).symm = conjNeg :=
  rfl

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