Theorems · Theorem · linear algebra

Matrix.permMatrix_mulVec

∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Fintype n] {v : n → R}
  [inst_2 : CommRing R], (Equiv.Perm.permMatrix R σ).mulVec v = v ∘ ⇑σ

Defined in

Mathlib.LinearAlgebra.Matrix.Permutation

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRing