theorem Vector.isEqv_iff_rel {α : Type u_1} {n : Nat} {a b : Vector α n} {r : α → α → Bool} : a.isEqv b r = true ↔ ∀ (i : Nat) (h' : i < n), r a[i] b[i] = true

theorem Vector.isEqv_eq_decide {α : Type u_1} {n : Nat} (a b : Vector α n) (r : α → α → Bool) : a.isEqv b r = decide (∀ (i : Nat) (h' : i < n), r a[i] b[i] = true)

@[simp]

theorem Vector.isEqv_toArray {α : Type u_1} {n : Nat} {r : α → α → Bool} [BEq α] (a b : Vector α n) : a.isEqv b.toArray r = a.isEqv b r

theorem Vector.eq_of_isEqv {α : Type u_1} {n : Nat} [DecidableEq α] (a b : Vector α n) (h : (a.isEqv b fun (x y : α) => decide (x = y)) = true) : a = b

theorem Vector.isEqv_self_beq {α : Type u_1} {n : Nat} [BEq α] [ReflBEq α] (a : Vector α n) : (a.isEqv a fun (x1 x2 : α) => x1 == x2) = true

theorem Vector.isEqv_self {α : Type u_1} {n : Nat} [DecidableEq α] (a : Vector α n) : (a.isEqv a fun (x1 x2 : α) => decide (x1 = x2)) = true

instance Vector.instDecidableEq {α : Type u_1} {n : Nat} [DecidableEq α] : DecidableEq (Vector α n)

Equations

• a.instDecidableEq b = match h : a.isEqv b fun (a b : α) => decide (a = b) with | true => isTrue ⋯ | false => isFalse ⋯

theorem Vector.beq_eq_decide {α : Type u_1} {n : Nat} [BEq α] (a b : Vector α n) : (a == b) = decide (∀ (i : Nat) (h' : i < n), (a[i] == b[i]) = true)

@[simp]

theorem Vector.beq_toArray {α : Type u_1} {n : Nat} [BEq α] (a b : Vector α n) : (a.toArray == b.toArray) = (a == b)

@[simp]

theorem Vector.beq_toList {α : Type u_1} {n : Nat} [BEq α] (a b : Vector α n) : (a.toList == b.toList) = (a == b)