transposeAddEquiv — Mathlib

English

There is an additive equivalence between m×n and n×m matrices given by transposition.

Русский

Существуют аддитивное эквивалентное отображение между матрицами размера m×n и n×m, задаваемое транспонированием.

LaTeX

$$$\mathrm{Transpose} : \mathrm{Mat}_{m\times n}(\alpha) \cong_+ \mathrm{Mat}_{n\times m}(\alpha)$ is an AddEquiv.$$

Lean4

/-- `Matrix.transpose` as an `AddEquiv` -/
@[simps apply]
def transposeAddEquiv [Add α] : Matrix m n α ≃+ Matrix n m α
    where
  toFun := transpose
  invFun := transpose
  left_inv := transpose_transpose
  right_inv := transpose_transpose
  map_add' := transpose_add

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