English
Let R be a semiring. For any matrices g ∈ M_{m×n}(R) and indices i, j ∈ n, let S be the column-swap permutation that interchanges the i-th and j-th columns. Then the (a, i)-entry of gS equals the (a, j)-entry of g, i.e. (gS)_{a i} = g_{a j} for every row a ∈ {1,…,m}.
Русский
Пусть R — полукольцо. Для любой матрицы g ∈ M_{m×n}(R) и индексов i, j ∈ {1,…,n}, обозначим S перестановку столбцов, которая меняет местами i-ю и j-ю столбцы. Тогда элемент в строке a и столбце i у произведения gS равен элементу в строке a и столбце j у g: (gS)_{a i} = g_{a j} для всех a.
LaTeX
$$$ (G \cdot \mathrm{swap}_{ij})_{a i} = G_{a j} $$$
Lean4
/-- Multiplying with `swap R i j` on the right swaps the `i`-th column with the `j`-th column. -/
@[simp]
theorem mul_swap_apply_left (i j : n) (a : m) (g : Matrix m n R) : (g * swap R i j) a i = g a j := by
simp [swap, PEquiv.mul_toMatrix_toPEquiv]
