mul_swap_apply_right — Mathlib

English

Let R be a semiring. For G ∈ M_{m×n}(R) and i, j ∈ n, the (a, j)-entry of G swap equals the (a, i)-entry of G, i.e. (G swap)_{a j} = G_{a i} for all a.

Русский

Пусть R — полукольцо. Для матрицы G ∈ M_{m×n}(R) и индексов i, j ∈ {1,…,n} имеем (G swap)_{a j} = G_{a i} для всех a.

LaTeX

$$$ (G \cdot \mathrm{swap}_{ij})_{a j} = G_{a i} $$$

Lean4

/-- Multiplying with `swap R i j` on the right swaps the `j`-th column with the `i`-th column. -/
@[simp]
theorem mul_swap_apply_right (i j : n) (a : m) (g : Matrix m n R) : (g * swap R i j) a j = g a i := by
  rw [swap_comm, mul_swap_apply_left]

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