swap — Mathlib

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

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