transpose_single — Mathlib

English

Transposing a single-entry matrix swaps its indices: transposition of E_{ij}(a) equals E_{ji}(a).

Русский

Транспонирование единичной матрицы E_{ij}(a) меняет индексы местами: E_{ij}(a)^T = E_{ji}(a).

LaTeX

$$$\mathrm{transpose}(\mathrm{single}_{ij}(a)) = \mathrm{single}_{ji}(a)$$$

Lean4

@[simp]
theorem transpose_single (i : m) (j : n) (a : α) : (single i j a)ᵀ = single j i a := by aesop (add unsafe unfold single)

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