swap_mulVec — Mathlib

English

Acting by swap on the left corresponds to precomposing with the swap permutation on the vector.

Русский

Действие множителя swap слева соответствует предкомпозицией с перестановкой swap на векторе.

LaTeX

$$$\\\\forall a: (n \\to R), (swap R i j) *\\\\Vec a = a \\\\circ \\mathrm{swap}(i,j)$$$

Lean4

theorem swap_mulVec (i j : n) (a : n → R) : swap R i j *ᵥ a = a ∘ Equiv.swap i j := by
  simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

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