vecMul_swap_apply

Mathlib.LinearAlgebra.Matrix.Swap

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

English

The i-th component of the vector after vecMul with swap equals the j-th component of the original.

Русский

После vecMul на i-й компоненте получаем j-ю компоненту исходного вектора.

LaTeX

$$$$ (a \\\\vphantom{a} \\\\_i * swap R i j) = a_j $$$$

Lean4

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

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

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

Разделы

Аффилиация

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