Theorems · Theorem · combinatorics

List.permutationsAux_cons

∀ {α : Type u_1} (t : α) (ts is : List α),
  (t :: ts).permutationsAux is =
    List.foldr (fun y r => (List.permutationsAux2 t ts r y id).2) (ts.permutationsAux (t :: is)) is.permutations

Defined in

Mathlib.Data.List.Permutation

Cited by

7 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound