English
The matrix corresponding to swapping two coordinates i and j is given by I_n − E_{ii} − E_{jj} + E_{ij} + E_{ji}, i.e., the matrix of the transposition (i j) equals the identity adjusted by ± unit basis matrices.
Русский
Матрица, соответствующая обмену двух координат i и j, равна I_n − E_{ii} − E_{jj} + E_{ij} + E_{ji}.
LaTeX
$$$(I_n) - E_{ii} - E_{jj} + E_{ij} + E_{ji}$$$
Lean4
theorem toMatrix_swap [DecidableEq n] [AddGroupWithOne α] (i j : n) :
(Equiv.swap i j).toPEquiv.toMatrix =
(1 : Matrix n n α) - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix +
(single j i).toMatrix :=
by
ext
dsimp [toMatrix, single, Equiv.swap_apply_def, Equiv.toPEquiv, one_apply]
split_ifs <;> simp_all
