swap_mul_apply_left — Mathlib

English

If a ≠ i and a ≠ j, then (swap R i j * g) a b = g a b for all g.

Русский

Если a не равно i и не равно j, то (swap R i j * g) a b = g a b для всякого g.

LaTeX

$$$$ (swap R i j * g) a b = g a b \\\\text{ when } a \neq i, a \neq j $$$$

Lean4

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

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