Theorems · Theorem · combinatorics

List.sym.eq_def

∀ {α : Type u_1} (x : ℕ) (x_1 : List α),
  List.sym x x_1 =
    match x, x_1 with
    | 0, x => [Sym.nil]
    | x, [] => []
    | n.succ, x :: xs => List.map (fun p => x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs

Defined in

Mathlib.Data.List.Sym

Cited by

0 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Quot.sound