structure Vector.Perm {α : Type u_1} {n : Nat} (as bs : Vector α n) : Prop

Perm as bs asserts that as and bs are permutations of each other.

This is a wrapper around List.Perm, and for now has much less API. For more complicated verification, use perm_iff_toList_perm and the List API.

• of_toArray_perm :: (
• toArray : as.Perm bs.toArray
• )

def Vector.«term_~_» : Lean.TrailingParserDescr

Perm as bs asserts that as and bs are permutations of each other.

This is a wrapper around List.Perm, and for now has much less API. For more complicated verification, use perm_iff_toList_perm and the List API.

Equations

• Vector.«term_~_» = Lean.ParserDescr.trailingNode `Vector.«term_~_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

theorem Vector.perm_iff_toArray_perm {α : Type u_1} {n : Nat} {as bs : Vector α n} : as.Perm bs ↔ as.Perm bs.toArray

theorem Vector.perm_iff_toList_perm {α : Type u_1} {n : Nat} {as bs : Vector α n} : as.Perm bs ↔ as.toList.Perm bs.toList

theorem Vector.Perm.of_toList_perm {α : Type u_1} {n : Nat} {as bs : Vector α n} : as.toList.Perm bs.toList → as.Perm bs

theorem Vector.Perm.toList {α : Type u_1} {n : Nat} {as bs : Vector α n} : as.Perm bs → as.toList.Perm bs.toList

@[simp]

theorem Vector.perm_mk {α : Type u_1} {n : Nat} (as bs : Array α) (ha : as.size = n) (hb : bs.size = n) : { toArray := as, size_toArray := ha }.Perm { toArray := bs, size_toArray := hb } ↔ as.Perm bs

theorem Vector.toArray_perm_iff {α : Type u_1} {n : Nat} (xs : Vector α n) (ys : Array α) : xs.Perm ys ↔ ∃ (h : ys.size = n), xs.Perm { toArray := ys, size_toArray := h }

theorem Vector.perm_toArray_iff {α : Type u_1} {n : Nat} (xs : Array α) (ys : Vector α n) : xs.Perm ys.toArray ↔ ∃ (h : xs.size = n), { toArray := xs, size_toArray := h }.Perm ys

@[simp]

theorem Vector.Perm.refl {α : Type u_1} {n : Nat} (xs : Vector α n) : xs.Perm xs

theorem Vector.Perm.rfl {α : Type u_1} {n : Nat} {xs : Vector α n} : xs.Perm xs

theorem Vector.Perm.of_eq {α : Type u_1} {n : Nat} {xs ys : Vector α n} (h : xs = ys) : xs.Perm ys

theorem Vector.Perm.symm {α : Type u_1} {n : Nat} {xs ys : Vector α n} (h : xs.Perm ys) : ys.Perm xs

theorem Vector.Perm.trans {α : Type u_1} {n : Nat} {xs ys zs : Vector α n} (h₁ : xs.Perm ys) (h₂ : ys.Perm zs) : xs.Perm zs

instance Vector.instTransPerm {α : Type u_1} {n : Nat} : Trans Perm Perm Perm

Equations

• Vector.instTransPerm = { trans := ⋯ }

theorem Vector.perm_comm {α : Type u_1} {n : Nat} {xs ys : Vector α n} : xs.Perm ys ↔ ys.Perm xs

theorem Vector.Perm.mem_iff {α : Type u_1} {n : Nat} {a : α} {xs ys : Vector α n} (p : xs.Perm ys) : a ∈ xs ↔ a ∈ ys

theorem Vector.Perm.append {α : Type u_1} {m n : Nat} {xs ys : Vector α m} {as bs : Vector α n} (p₁ : xs.Perm ys) (p₂ : as.Perm bs) : (xs ++ as).Perm (ys ++ bs)

theorem Vector.Perm.push {α : Type u_1} {n : Nat} (x : α) {xs ys : Vector α n} (p : xs.Perm ys) : (xs.push x).Perm (ys.push x)

theorem Vector.Perm.push_comm {α : Type u_1} {n : Nat} (x y : α) {xs ys : Vector α n} (p : xs.Perm ys) : ((xs.push x).push y).Perm ((ys.push y).push x)

theorem Vector.swap_perm {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} (h₁ : i < n) (h₂ : j < n) : (xs.swap i j h₁ h₂).Perm xs

theorem Vector.Perm.extract {α : Type u_1} {n : Nat} {xs ys : Vector α n} (h : xs.Perm ys) {lo hi : Nat} (wlo : ∀ (i : Nat), i < lo → xs[i]? = ys[i]?) (whi : ∀ (i : Nat), hi ≤ i → xs[i]? = ys[i]?) : (xs.extract lo hi).Perm (ys.extract lo hi)