permMatrix_mulVec

Mathlib.LinearAlgebra.Matrix.Permutation

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

← MathLib Explorer

English

Same as above, in a simplified form.

Русский

То же самое в упрощённой форме.

LaTeX

$$$\\sigma\\text{.permMatrix }R \\cdot v = v \\circ \\sigma$$$

Lean4

theorem permMatrix_mulVec {v : n → R} [CommRing R] : σ.permMatrix R *ᵥ v = v ∘ σ :=
  by
  ext j
  simp [mulVec_eq_sum, Pi.single, Function.update, Equiv.eq_symm_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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