Documentation Verification Report

Fold

📁 Source: Mathlib/Data/Multiset/Fold.lean

Statistics

Metric	Count
Definitions `fold`	1
Theorems `coe_fold_l`, `coe_fold_r`, `fold_add`, `fold_cons'_left`, `fold_cons'_right`, `fold_cons_left`, `fold_cons_right`, `fold_dedup_idem`, `fold_distrib`, `fold_eq_foldl`, `fold_eq_foldr`, `fold_hom`, `fold_singleton`, `fold_union_inter`, `fold_zero`	15
Total	16

Multiset

Definitions

Name	Category	Theorems
`fold` 📖	CompOp	18 math math: `fold_cons_left`, `noncommFold_eq_fold`, `fold_union_inter`, `fold_add`, `fold_cons'_left`, `fold_eq_foldl`, `fold_zero`, `fold_eq_foldr`, `fold_dedup_idem`, `fold_bind`, `fold_hom`, `coe_fold_l`, `max_le_of_forall_le`, `fold_singleton`, `coe_fold_r`, `fold_cons'_right`, `fold_distrib`, `fold_cons_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_fold_l` 📖	mathematical	—	`fold` `ofList`	—	`instLeftCommutativeOfCommutativeOfAssociative` `coe_foldr_swap`
`coe_fold_r` 📖	mathematical	—	`fold` `ofList`	—	—
`fold_add` 📖	mathematical	—	`fold` `Multiset` `instAdd`	—	`induction_on` `add_zero` `fold_zero` `fold_cons'_right` `fold_cons_right` `fold_cons_left` `add_cons`
`fold_cons'_left` 📖	mathematical	—	`fold` `cons`	—	`fold_cons'_right`
`fold_cons'_right` 📖	mathematical	—	`fold` `cons`	—	`instRightCommutativeOfCommutativeOfAssociative` `fold_eq_foldl` `foldl_cons`
`fold_cons_left` 📖	mathematical	—	`fold` `cons`	—	`foldr_cons` `instLeftCommutativeOfCommutativeOfAssociative`
`fold_cons_right` 📖	mathematical	—	`fold` `cons`	—	`fold_cons_left`
`fold_dedup_idem` 📖	mathematical	—	`fold` `dedup`	—	`induction_on` `fold.congr_simp` `dedup_cons_of_mem` `fold_cons_left` `cons_erase` `dedup_cons_of_notMem`
`fold_distrib` 📖	mathematical	—	`fold` `map`	—	`induction_on` `map_cons` `fold_cons_left` `fold_cons_right`
`fold_eq_foldl` 📖	mathematical	—	`fold` `foldl` `instRightCommutativeOfCommutativeOfAssociative`	—	`instRightCommutativeOfCommutativeOfAssociative` `coe_fold_l`
`fold_eq_foldr` 📖	mathematical	—	`fold` `foldr` `instLeftCommutativeOfCommutativeOfAssociative`	—	—
`fold_hom` 📖	mathematical	—	`fold` `map`	—	`induction_on` `fold.congr_simp` `map_cons` `fold_cons_left`
`fold_singleton` 📖	mathematical	—	`fold` `Multiset` `instSingleton`	—	`foldr_singleton` `instLeftCommutativeOfCommutativeOfAssociative`
`fold_union_inter` 📖	mathematical	—	`fold` `Multiset` `instUnion` `instInter`	—	`fold_add` `union_add_inter`
`fold_zero` 📖	mathematical	—	`fold` `Multiset` `instZero`	—	—

---

← Back to Index