English
The swap matrix is the permutation matrix corresponding to exchanging two indices.
Русский
Матрица перестановки соответствует замене двух индексов.
LaTeX
$$$swap(R,i,j) = PermutationMatrix(Equiv.swap(i,j))$$$
Lean4
/-- The swap matrix `swap R i j` is the identity matrix with the
`i`-th and `j`-th rows modified such that multiplying by it on the
left (resp. right) corresponds to swapping the `i`-th and `j`-th row (resp. column). -/
def swap (i j : n) : Matrix n n R :=
(Equiv.swap i j).permMatrix R