swap_mulVec_apply

Mathlib.LinearAlgebra.Matrix.Swap

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

English

The i-th component of the left-multiplied vector is the j-th component of the original vector.

Русский

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

LaTeX

$$$$(swap R i j) *\\\\mathbf{v} \\\\_i = v_j$$$$

Lean4

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

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

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

Разделы

Аффилиация

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