transpose_swap

Mathlib.LinearAlgebra.Matrix.Swap

URI: https://scilib.ai/kg/mathlib#Matrix.transpose_swap

English

The transpose of a swap matrix equals itself.

Русский

Транспонированная матрица перестановки равна самой себе.

LaTeX

$$$(swap(R,i,j)).^T = swap(R,i,j)$$$

Lean4

@[simp]
theorem transpose_swap (i j : n) : (swap R i j).transpose = swap R i j := by simp [swap]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru