The vecPerm simproc

The vecPerm simproc computes the new entries of a vector after applying a permutation to them.

def Mathlib.Tactic.FinVec.vecPerm : Lean.Meta.Simp.Simproc

The vecPerm simproc computes the new entries of a vector after applying a permutation to them. This can be used to simplify expressions as follows:

example {a b c : Nat} : ![a, b, c] ∘ Equiv.swap 0 1 = ![b, a, c] := by
  simp [vecPerm, Equiv.swap_apply_def]

Note that for this simproc to work, dsimp needs to be able to simplify the individual applications of the permutation.

Equations

• One or more equations did not get rendered due to their size.