Documentation

Mathlib.Data.Array.Defs

Definitions on Arrays #

This file contains various definitions on Array. It does not contain proofs about these definitions, those are contained in other files in Mathlib.Data.Array.

def Array.cyclicPermute! {α : Type u_1} [Inhabited α] :
Array αList NatArray α

Permute the array using a sequence of indices defining a cyclic permutation. If the list of indices l = [i₁, i₂, ..., iₙ] are all distinct then (cyclicPermute! a l)[iₖ₊₁] = a[iₖ] and (cyclicPermute! a l)[i₀] = a[iₙ]

Equations
Instances For
    def Array.cyclicPermute!.cyclicPermuteAux {α : Type u_1} :
    Array αList NatαNatArray α
    Equations
    Instances For
      def Array.permute! {α : Type u_1} [Inhabited α] (a : Array α) (ls : List (List Nat)) :

      Permute the array using a list of cycles.

      Equations
      Instances For