English
Let A be an m×n matrix over a ring R. The vectorization of A transposed is obtained from the vectorization of A by applying the index-swap permutation; equivalently, vec(A^T) is vec(A) with the indices swapped.
Русский
Пусть A — матрица размера m×n над кольцом R. Векторизация транспонированной матрицы равна векторизации исходной матрицы после применения перестановки индексов (i,j)↔(j,i).
LaTeX
$$$$\operatorname{vec}(A^{\top}) = \operatorname{vec}(A) \circ \mathrm{swap}$$$$
Lean4
theorem vec_transpose (A : Matrix m n R) : vec Aᵀ = vec A ∘ Prod.swap :=
rfl