swap_mul_apply_right — Mathlib

English

Multiplying on the left by swap exchanges the i-th and j-th rows; equivalently, multiplying on the left with swap swaps the j-th row with the i-th.

Русский

Умножение слева на swap меняет местами i-ю и j-ю строки; эквивалентно обмену j-й строки с i-й.

LaTeX

$$$swap(R,i,j) * g$ имеет строку $i$ равную строке $j$ матрицы $g$$$

Lean4

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

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