Definition and basic properties of List.offDiag

In this file we define List.offDiag l to be the product l.product l with the diagonal removed. The actual definition is more complicated to avoid assuming that equality on α is decidable.

def List.offDiag {α : Type u_1} (l : List α) : List (α × α)

List.offDiag lis the productl.product l` with the diagonal removed.

Equations

• l.offDiag = List.flatMap (fun (x : α × ℕ) => match x with | (x, n) => List.map (Prod.mk x) (l.eraseIdx n)) l.zipIdx

@[simp]

theorem List.offDiag_nil {α : Type u_1} : [].offDiag = []

theorem List.offDiag_cons_perm {α : Type u_1} (a : α) (l : List α) : (a :: l).offDiag.Perm (map (fun (x : α) => (a, x)) l ++ map (fun (x : α) => (x, a)) l ++ l.offDiag)

@[simp]

theorem List.offDiag_singleton {α : Type u_1} (a : α) : [a].offDiag = []

theorem List.length_offDiag' {α : Type u_1} (l : List α) : l.offDiag.length = l.length * (l.length - 1)

@[simp]

theorem List.length_offDiag {α : Type u_1} (l : List α) : l.offDiag.length = l.length ^ 2 - l.length

theorem List.mem_offDiag_iff_getElem {α : Type u_1} {l : List α} {x : α × α} : x ∈ l.offDiag ↔ ∃ (i : ℕ), ∃ (x_1 : i < l.length), ∃ (j : ℕ), ∃ (x_2 : j < l.length), i ≠ j ∧ l[i] = x.fst ∧ l[j] = x.snd

theorem List.count_offDiag_eq_mul_sub_ite {α : Type u_1} [DecidableEq α] (l : List α) (a b : α) : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0

theorem List.Perm.offDiag {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) : l₁.offDiag.Perm l₂.offDiag

theorem List.Nodup.offDiag {α : Type u_1} {l : List α} (h : l.Nodup) : l.offDiag.Nodup

theorem List.Nodup.of_offDiag {α : Type u_1} {l : List α} (h : l.offDiag.Nodup) : l.Nodup

@[simp]

theorem List.nodup_offDiag {α : Type u_1} {l : List α} : l.offDiag.Nodup ↔ l.Nodup

List.offDiag l has no duplicates iff the original list has no duplicates.

theorem List.Nodup.mem_offDiag {α : Type u_1} {l : List α} (h : l.Nodup) {x : α × α} : x ∈ l.offDiag ↔ x.fst ∈ l ∧ x.snd ∈ l ∧ x.fst ≠ x.snd

If l : List α is a list with no duplicates, then x : α × α belongs to List.offDiag l iff both components of x belong to l and they are not equal.

theorem List.map_prodMap_offDiag {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : map (Prod.map f f) l.offDiag = (map f l).offDiag