Documentation

Mathlib.Data.List.OffDiag

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.

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

List.offDiag l is the product l.product l with the diagonal removed.

Instances For
    source
    📐 coverage
    @[simp]
    theorem List.offDiag_nil {α : Type u_1} :
    [].offDiag = []
    source
    📐 coverage
    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)
    source
    📐 coverage
    @[simp]
    theorem List.offDiag_singleton {α : Type u_1} (a : α) :
    [a].offDiag = []
    source
    📐 coverage
    theorem List.length_offDiag' {α : Type u_1} (l : List α) :
    l.offDiag.length = l.length * (l.length - 1)
    source
    📐 coverage
    @[simp]
    theorem List.length_offDiag {α : Type u_1} (l : List α) :
    l.offDiag.length = l.length ^ 2 - l.length
    source
    📐 coverage
    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.1 ∧ l[j] = x.2
    source
    📐 coverage
    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
    source
    📐 coverage
    theorem List.Perm.offDiag {α : Type u_1} {l₁ l₂ : List α} (h : l₁.Perm l₂) :
    l₁.offDiag.Perm l₂.offDiag
    source
    📐 coverage
    theorem List.Nodup.offDiag {α : Type u_1} {l : List α} (h : l.Nodup) :
    l.offDiag.Nodup
    source
    theorem List.Nodup.of_offDiag {α : Type u_1} {l : List α} (h : l.offDiag.Nodup) :
    l.Nodup
    source
    📐 coverage
    @[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.

    source
    📐 coverage
    theorem List.Nodup.mem_offDiag {α : Type u_1} {l : List α} (h : l.Nodup) {x : α × α} :
    x ∈ l.offDiag ↔ x.1 ∈ l ∧ x.2 ∈ l ∧ x.1 ≠ x.2

    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.

    source
    📐 coverage
    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