transposeLinearEquiv_symm — Mathlib

English

The transpose linear equivalence is symmetric in its arguments, i.e., its inverse is the transpose in the swapped indices.

Русский

Транспонирование как линейное эквивалентность симметрично по аргументам: обратное отображение — транспонирование с переставленными индексами.

LaTeX

$$$(\mathrm{transposeLinearEquiv}(m,n,\alpha))^{-1} = \mathrm{transposeLinearEquiv}(n,m,\alpha).$$$

Lean4

@[simp]
theorem transposeLinearEquiv_symm [Semiring R] [AddCommMonoid α] [Module R α] :
    (transposeLinearEquiv m n R α).symm = transposeLinearEquiv n m R α :=
  rfl

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