Documentation Verification Report

Basic

📁 Source: Mathlib/Data/List/Perm/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `eraseIdx_of_getElem?_eq`, `flatMap`, `flatMap_left`, `foldl_eq`, `foldl_op_eq`, `foldr_eq`, `foldr_op_eq`, `insertIdx`, `insertIdx_of_le`, `product`, `product_left`, `product_right`, `subset_congr_left`, `subset_congr_right`, `count_eq_count_filter_add`, `eq_map_comp_perm`, `flatMap_append_perm`, `forall₂_comp_perm_eq_perm_comp_forall₂`, `getElem_cons_eraseIdx_perm`, `instSymmPerm_mathlib`, `map_append_flatMap_perm`, `map_perm_map_iff`, `perm_comp_forall₂`, `perm_comp_perm`, `perm_eraseIdx_of_getElem?_eq`, `perm_insertIdx_iff`, `perm_insertIdx_iff_of_le`, `perm_option_toList`, `perm_replicate_append_replicate`, `perm_rfl`, `rel_perm`, `rel_perm_imp`, `set_perm_cons_eraseIdx`	33
Total	33

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_eq_count_filter_add` 📖	—	—	—	—	—
`eq_map_comp_perm` 📖	mathematical	—	`Relation.Comp`	—	`Relation.comp_eq_fun` `forall₂_comp_perm_eq_perm_comp_forall₂`
`flatMap_append_perm` 📖	—	—	—	—	—
`forall₂_comp_perm_eq_perm_comp_forall₂` 📖	mathematical	—	`Relation.Comp`	—	`Forall₂.flip` `perm_comp_forall₂`
`getElem_cons_eraseIdx_perm` 📖	—	—	—	—	`set_perm_cons_eraseIdx`
`instSymmPerm_mathlib` 📖	—	—	—	—	—
`map_append_flatMap_perm` 📖	—	—	—	—	`flatMap_append_perm`
`map_perm_map_iff` 📖	—	—	—	—	`eq_map_comp_perm`
`perm_comp_forall₂` 📖	mathematical	—	`Relation.Comp`	—	—
`perm_comp_perm` 📖	mathematical	—	`Relation.Comp`	—	—
`perm_eraseIdx_of_getElem?_eq` 📖	—	—	—	—	`rel_congr_left` `instSymmPerm_mathlib` `instIsTransOfTrans` `getElem_cons_eraseIdx_perm` `rel_congr_right`
`perm_insertIdx_iff` 📖	—	—	—	—	`perm_insertIdx_iff_of_le`
`perm_insertIdx_iff_of_le` 📖	—	—	—	—	`rel_congr_left` `instSymmPerm_mathlib` `instIsTransOfTrans` `rel_congr_right`
`perm_option_toList` 📖	—	—	—	—	—
`perm_replicate_append_replicate` 📖	—	—	—	—	`Decidable.and_forall_ne` `not_imp_not`
`perm_rfl` 📖	—	—	—	—	—
`rel_perm` 📖	mathematical	`Relator.BiUnique`	`Relator.LiftFun`	—	`rel_perm_imp` `Relator.LeftUnique.flip` `Forall₂.flip`
`rel_perm_imp` 📖	mathematical	`Relator.RightUnique`	`Relator.LiftFun`	—	`Relation.comp_assoc` `forall₂_comp_perm_eq_perm_comp_forall₂` `right_unique_forall₂'`
`set_perm_cons_eraseIdx` 📖	—	—	—	—	`insertIdx_eraseIdx_self`

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eraseIdx_of_getElem?_eq` 📖	—	—	—	—	`List.perm_eraseIdx_of_getElem?_eq`
`flatMap` 📖	—	—	—	—	`flatMap_left`
`flatMap_left` 📖	—	—	—	—	`List.forall₂_map_right_iff` `List.forall₂_map_left_iff` `List.forall₂_same`
`foldl_eq` 📖	—	—	—	—	`RightCommutative.right_comm`
`foldl_op_eq` 📖	—	—	—	—	`foldl_eq` `instRightCommutativeOfCommutativeOfAssociative`
`foldr_eq` 📖	—	—	—	—	`LeftCommutative.left_comm`
`foldr_op_eq` 📖	—	—	—	—	`foldr_eq` `instLeftCommutativeOfCommutativeOfAssociative`
`insertIdx` 📖	—	—	—	—	`List.perm_insertIdx_iff`
`insertIdx_of_le` 📖	—	—	—	—	`List.perm_insertIdx_iff_of_le`
`product` 📖	—	—	—	—	`product_right` `product_left`
`product_left` 📖	—	—	—	—	`flatMap_left`
`product_right` 📖	—	—	—	—	—
`subset_congr_left` 📖	—	—	—	—	—
`subset_congr_right` 📖	—	—	—	—	—

---

← Back to Index