vecMul_swap

Mathlib.LinearAlgebra.Matrix.Swap

URI: https://scilib.ai/kg/mathlib#Matrix.vecMul_swap

English

The vector-multiplication by a on a swap equals the composition with swap.

Русский

Умножение вектора слева на swap равно композиции с перестановкой swap.

LaTeX

$$$\\\\forall a, (a \\\\mathbf{v}* swap R i j) = a \\\\circ (Equiv.swap i j)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru