conjTransposeLinearEquiv_symm — Mathlib

English

The symmetry of conjTransposeLinearEquiv asserts that its inverse equals the same construction with swapped indices: (conjTransposeLinearEquiv m n α).symm = conjTransposeLinearEquiv n m α.

Русский

Симметрия линейного эквивалента сопряжённого транспонирования: (conjTransposeLinearEquiv m n α).symm = conjTransposeLinearEquiv n m α.

LaTeX

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

Lean4

@[simp]
theorem conjTransposeLinearEquiv_symm [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α] [Module R α]
    [StarModule R α] : (conjTransposeLinearEquiv m n R α).symm = conjTransposeLinearEquiv n m R α :=
  rfl

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