conjTransposeAddEquiv_symm — Mathlib

English

The inverse of conjTransposeAddEquiv equals conjTransposeAddEquiv with the arguments swapped: (conjTransposeAddEquiv m n α).symm = conjTransposeAddEquiv n m α.

Русский

Обратное отображение conjTransposeAddEquiv равно conjTransposeAddEquiv с поменянными параметрами: (conjTransposeAddEquiv m n α).symm = conjTransposeAddEquiv n m α.

LaTeX

$$$ (conjTransposeAddEquiv\, m\, n\, α).symm = conjTransposeAddEquiv\, n\, m\, α $$$

Lean4

@[simp]
theorem conjTransposeAddEquiv_symm [AddMonoid α] [StarAddMonoid α] :
    (conjTransposeAddEquiv m n α).symm = conjTransposeAddEquiv n m α :=
  rfl

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