Permutation

📁 Source: Mathlib/Data/List/Permutation.lean

Statistics

Metric	Count
Definitions	0
Theorems `permutations`, `permutations'`, `count_permutations'Aux_self`, `foldr_permutationsAux2`, `getElem_permutations'Aux`, `get_permutations'Aux`, `injective_permutations'Aux`, `length_foldr_permutationsAux2`, `length_foldr_permutationsAux2'`, `length_permutations`, `length_permutations'Aux`, `length_permutationsAux`, `length_permutationsAux2`, `map_map_permutations'Aux`, `map_map_permutationsAux2`, `map_permutations`, `map_permutations'`, `map_permutationsAux`, `map_permutationsAux2`, `map_permutationsAux2'`, `mem_foldr_permutationsAux2`, `mem_permutations`, `mem_permutations'`, `mem_permutationsAux2`, `mem_permutationsAux2'`, `mem_permutationsAux_of_perm`, `mem_permutations_of_perm_lemma`, `nodup_permutations`, `nodup_permutations'Aux_iff`, `nodup_permutations'Aux_of_notMem`, `nodup_permutations_iff`, `perm_of_mem_permutations`, `perm_of_mem_permutationsAux`, `perm_permutations'Aux_comm`, `perm_permutations'_iff`, `perm_permutations_iff`, `permutations'Aux_eq_permutationsAux2`, `permutationsAux2_append`, `permutationsAux2_comp_append`, `permutationsAux2_fst`, `permutationsAux2_snd_cons`, `permutationsAux2_snd_eq`, `permutationsAux2_snd_nil`, `permutationsAux_append`, `permutationsAux_cons`, `permutationsAux_nil`, `permutations_append`, `permutations_nil`, `permutations_perm_permutations'`, `permutations_take_two`	50
Total	50

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_permutations'Aux_self` 📖	mathematical	—	`permutations'Aux`	—	`permutations'Aux.eq_2` `count_map_of_injective`
`foldr_permutationsAux2` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_append`
`getElem_permutations'Aux` 📖	—	`permutations'Aux`	—	—	—
`get_permutations'Aux` 📖	—	`permutations'Aux`	—	—	`getElem_permutations'Aux`
`injective_permutations'Aux` 📖	mathematical	—	`permutations'Aux`	—	`insertIdx_injective` `length_permutations'Aux` `get_permutations'Aux`
`length_foldr_permutationsAux2` 📖	mathematical	—	`permutationsAux2`	—	`foldr_permutationsAux2` `length_permutationsAux2`
`length_foldr_permutationsAux2'` 📖	mathematical	—	`permutationsAux2`	—	`length_foldr_permutationsAux2`
`length_permutations` 📖	mathematical	—	`permutations` `Nat.factorial`	—	`length_permutationsAux`
`length_permutations'Aux` 📖	mathematical	—	`permutations'Aux`	—	—
`length_permutationsAux` 📖	mathematical	—	`permutationsAux` `Nat.factorial`	—	`permutationsAux_nil` `permutationsAux_cons` `length_foldr_permutationsAux2'` `perm_of_mem_permutations` `permutations.eq_1` `Nat.factorial_succ`
`length_permutationsAux2` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_snd_cons`
`map_map_permutations'Aux` 📖	mathematical	—	`permutations'Aux`	—	—
`map_map_permutationsAux2` 📖	mathematical	—	`permutationsAux2`	—	`map_permutationsAux2'`
`map_permutations` 📖	mathematical	—	`permutations`	—	`permutations.eq_1` `map_permutationsAux`
`map_permutations'` 📖	mathematical	—	`permutations'`	—	—
`map_permutationsAux` 📖	mathematical	—	`permutationsAux`	—	`permutationsAux_nil` `permutationsAux_cons` `foldr_permutationsAux2` `map_map_permutationsAux2`
`map_permutationsAux2` 📖	mathematical	—	`permutationsAux2`	—	`map_permutationsAux2'`
`map_permutationsAux2'` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_snd_cons`
`mem_foldr_permutationsAux2` 📖	mathematical	—	`permutationsAux2`	—	`foldr_permutationsAux2`
`mem_permutations` 📖	mathematical	—	`permutations`	—	`perm_of_mem_permutations` `mem_permutations_of_perm_lemma` `mem_permutationsAux_of_perm`
`mem_permutations'` 📖	mathematical	—	`permutations'`	—	`permutations_perm_permutations'` `mem_permutations`
`mem_permutationsAux2` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_snd_cons`
`mem_permutationsAux2'` 📖	mathematical	—	`permutationsAux2`	—	`mem_permutationsAux2`
`mem_permutationsAux_of_perm` 📖	mathematical	—	`permutationsAux`	—	`permutationsAux_nil` `permutationsAux_cons` `mem_foldr_permutationsAux2` `mem_permutations_of_perm_lemma`
`mem_permutations_of_perm_lemma` 📖	mathematical	`permutationsAux`	`permutations`	—	—
`nodup_permutations` 📖	mathematical	—	`permutations`	—	`permutations_perm_permutations'` `permutations'.eq_2` `nodup_flatMap` `nodup_permutations'Aux_iff` `mem_permutations'` `Nodup.pairwise_of_forall_ne` `Function.onFun.eq_1` `length_permutations'Aux` `get_permutations'Aux` `lt_trichotomy` `insertIdx_injective`
`nodup_permutations'Aux_iff` 📖	mathematical	—	`permutations'Aux`	—	`length_permutations'Aux` `LT.lt.le` `nodup_iff_injective_get` `get_permutations'Aux` `nodup_permutations'Aux_of_notMem`
`nodup_permutations'Aux_of_notMem` 📖	mathematical	—	`permutations'Aux`	—	`nodup_map_iff`
`nodup_permutations_iff` 📖	mathematical	—	`permutations`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `exists_duplicate_iff_not_nodup` `duplicate_iff_sublist` `Perm.permutations` `permutations_take_two` `nodup_permutations`
`perm_of_mem_permutations` 📖	—	`permutations`	—	—	`perm_of_mem_permutationsAux`
`perm_of_mem_permutationsAux` 📖	—	`permutationsAux`	—	—	`permutationsAux_nil` `instIsEmptyFalse` `mem_foldr_permutationsAux2` `permutations.eq_1` `permutationsAux_cons`
`perm_permutations'Aux_comm` 📖	mathematical	—	`permutations'Aux`	—	`flatMap_append_perm`
`perm_permutations'_iff` 📖	mathematical	—	`permutations'`	—	`mem_permutations'` `Perm.permutations'`
`perm_permutations_iff` 📖	mathematical	—	`permutations`	—	`mem_permutations` `Perm.permutations`
`permutations'Aux_eq_permutationsAux2` 📖	mathematical	—	`permutations'Aux` `permutationsAux2`	—	`permutationsAux2_snd_cons` `map_permutationsAux2`
`permutationsAux2_append` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_snd_cons`
`permutationsAux2_comp_append` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_snd_cons`
`permutationsAux2_fst` 📖	mathematical	—	`permutationsAux2`	—	—
`permutationsAux2_snd_cons` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_fst`
`permutationsAux2_snd_eq` 📖	mathematical	—	`permutationsAux2`	—	`permutationsAux2_append` `map_permutationsAux2` `permutationsAux2_comp_append`
`permutationsAux2_snd_nil` 📖	mathematical	—	`permutationsAux2`	—	—
`permutationsAux_append` 📖	mathematical	—	`permutationsAux`	—	`permutationsAux_nil` `permutationsAux_cons` `foldr_permutationsAux2` `map_permutationsAux2`
`permutationsAux_cons` 📖	mathematical	—	`permutationsAux` `permutationsAux2` `permutations`	—	`permutationsAux.eq_1`
`permutationsAux_nil` 📖	mathematical	—	`permutationsAux`	—	`permutationsAux.eq_1`
`permutations_append` 📖	mathematical	—	`permutations` `permutationsAux`	—	`permutationsAux_append`
`permutations_nil` 📖	mathematical	—	`permutations`	—	`permutations.eq_1` `permutationsAux_nil`
`permutations_perm_permutations'` 📖	mathematical	—	`permutations` `permutations'`	—	`permutationsAux_nil` `Perm.permutations'` `permutations_append` `permutationsAux_cons` `foldr_permutationsAux2` `permutations'.eq_2` `flatMap_append_perm` `permutations'Aux_eq_permutationsAux2` `permutationsAux2_append`
`permutations_take_two` 📖	mathematical	—	`permutations`	—	`permutationsAux_cons` `permutationsAux_nil` `permutationsAux2_snd_cons`

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`permutations` 📖	mathematical	—	`List.permutations`	—	`List.permutations_perm_permutations'` `permutations'`
`permutations'` 📖	mathematical	—	`List.permutations'`	—	`flatMap_left` `List.perm_permutations'Aux_comm`

---

← Back to Index