vecMul_permMatrix — Mathlib

English

Left vector-matrix multiplication corresponds to composing with the inverse permutation.

Русский

Левое умножение вектора на матрицу перестановки соответствует композиции с обратной перестановкой.

LaTeX

$$$v^{\\mathrm{T}} P_{\\sigma} = v^{\\mathrm{T}} \\! \\circ \\sigma^{-1}$$$

Lean4

theorem vecMul_permMatrix {v : n → R} [CommRing R] : v ᵥ* σ.permMatrix R = v ∘ σ.symm :=
  by
  ext j
  simp [vecMul_eq_sum, Pi.single, Function.update, ← Equiv.symm_apply_eq]

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