mul_swap_of_ne — Mathlib

English

Let R be a semiring. If b ≠ i and b ≠ j, then the (a, b)-entry of g swap equals the (a, b)-entry of g, i.e. (g swap)_{a b} = g_{a b} for all a.

Русский

Пусть R — полукольцо. Если b ≠ i и b ≠ j, то элемент (a, b) в g swap равен элементу (a, b) в g: (g swap)_{a b} = g_{a b} для всех a.

LaTeX

$$$ (G \cdot \mathrm{swap}_{ij})_{a b} = G_{a b} \quad\text{если } b \neq i \land b \neq j $$$

Lean4

theorem mul_swap_of_ne {i j b : n} {a : m} (hbi : b ≠ i) (hbj : b ≠ j) (g : Matrix m n R) :
    (g * swap R i j) a b = g a b := by simp [swap, PEquiv.mul_toMatrix_toPEquiv, Equiv.swap_apply_of_ne_of_ne hbi hbj]

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