transposeLinearEquiv — Mathlib

English

The transpose defines a linear equivalence between the space of m×n matrices and the space of n×m matrices.

Русский

Транспонирование задаёт линейное эквивалентное отображение между пространствами матриц размерности m×n и n×m.

LaTeX

$$$\mathrm{transposeAddEquiv}(m,n,\alpha) : \mathrm{Mat}_{m\times n}(\alpha) \simeq_+ \mathrm{Mat}_{n\times m}(\alpha)$ is a linear equivalence.$$

Lean4

/-- `Matrix.transpose` as a `LinearMap` -/
@[simps apply]
def transposeLinearEquiv [Semiring R] [AddCommMonoid α] [Module R α] : Matrix m n α ≃ₗ[R] Matrix n m α :=
  { transposeAddEquiv m n α with map_smul' := transpose_smul }

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