swap_mul_self — Mathlib

English

A swap permutation matrix is its own inverse; i.e., swapping twice yields the identity: S^2 = I.

Русский

Перестановочная матрица обмена является своей собственной обратной: обмен выполняется дважды подряд — получаем тождественную матрицу.

LaTeX

$$$ \mathrm{swap}_{ij}^2 = I $$$

Lean4

/-- Swap matrices are self inverse. -/
theorem swap_mul_self (i j : n) : swap R i j * swap R i j = 1 :=
  by
  simp only [swap]
  rw [← Equiv.swap_inv, Equiv.Perm.inv_def]
  simp [← PEquiv.toMatrix_trans, ← Equiv.toPEquiv_trans]

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