Documentation Verification Report

Fold

📁 Source: Mathlib/Control/Fold.lean

Statistics

Metric	Count
Definitions `Foldl`, `get`, `mk`, `ofFreeMonoid`, `Foldr`, `get`, `mk`, `ofFreeMonoid`, `foldlM`, `get`, `mk`, `ofFreeMonoid`, `foldrM`, `get`, `mk`, `ofFreeMonoid`, `foldMap`, `foldl`, `foldlm`, `foldr`, `foldrm`, `length`, `mapFold`, `toList`	24
Theorems `ofFreeMonoid_apply`, `ofFreeMonoid_apply`, `ofFreeMonoid_apply`, `ofFreeMonoid_apply`, `map_eq_map`, `foldMap_hom`, `foldMap_hom_free`, `foldMap_map`, `ofFreeMonoid_comp_of`, `unop_ofFreeMonoid`, `foldl_map`, `foldl_toList`, `ofFreeMonoid_comp_of`, `foldlm_map`, `foldlm_toList`, `ofFreeMonoid_comp_of`, `foldr_map`, `foldr_toList`, `ofFreeMonoid_comp_of`, `foldrm_map`, `foldrm_toList`, `length_toList`, `toList_eq_self`, `toList_map`, `toList_spec`	25
Total	49

Monoid

Definitions

Name	Category	Theorems
`Foldl` 📖	CompOp	3 math math: `Foldl.ofFreeMonoid_apply`, `Traversable.foldl.unop_ofFreeMonoid`, `Traversable.foldl.ofFreeMonoid_comp_of`
`Foldr` 📖	CompOp	2 math math: `Traversable.foldr.ofFreeMonoid_comp_of`, `Foldr.ofFreeMonoid_apply`
`foldlM` 📖	CompOp	2 math math: `Traversable.foldlm.ofFreeMonoid_comp_of`, `foldlM.ofFreeMonoid_apply`
`foldrM` 📖	CompOp	2 math math: `Traversable.foldrm.ofFreeMonoid_comp_of`, `foldrM.ofFreeMonoid_apply`

Monoid.Foldl

Definitions

Name	Category	Theorems
`get` 📖	CompOp	—
`mk` 📖	CompOp	—
`ofFreeMonoid` 📖	CompOp	3 math math: `ofFreeMonoid_apply`, `Traversable.foldl.unop_ofFreeMonoid`, `Traversable.foldl.ofFreeMonoid_comp_of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `Monoid.Foldl` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MulOpposite.instMulOne` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `ofFreeMonoid` `MulOpposite.op` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.toList`	—	—

Monoid.Foldr

Definitions

Name	Category	Theorems
`get` 📖	CompOp	—
`mk` 📖	CompOp	—
`ofFreeMonoid` 📖	CompOp	2 math math: `Traversable.foldr.ofFreeMonoid_comp_of`, `ofFreeMonoid_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `Monoid.Foldr` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `CategoryTheory.End.monoid` `CategoryTheory.types` `MonoidHom.instFunLike` `ofFreeMonoid` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.toList`	—	—

Monoid.foldlM

Definitions

Name	Category	Theorems
`get` 📖	CompOp	—
`mk` 📖	CompOp	—
`ofFreeMonoid` 📖	CompOp	2 math math: `Traversable.foldlm.ofFreeMonoid_comp_of`, `ofFreeMonoid_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `Monoid.foldlM` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MulOpposite.instMulOne` `CategoryTheory.End` `CategoryTheory.KleisliCat` `CategoryTheory.KleisliCat.categoryStruct` `CategoryTheory.End.monoid` `CategoryTheory.KleisliCat.category` `MonoidHom.instFunLike` `ofFreeMonoid` `MulOpposite.op` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.toList`	—	—

Monoid.foldrM

Definitions

Name	Category	Theorems
`get` 📖	CompOp	—
`mk` 📖	CompOp	—
`ofFreeMonoid` 📖	CompOp	2 math math: `Traversable.foldrm.ofFreeMonoid_comp_of`, `ofFreeMonoid_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `Monoid.foldrM` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `CategoryTheory.End.monoid` `CategoryTheory.KleisliCat` `CategoryTheory.KleisliCat.category` `MonoidHom.instFunLike` `ofFreeMonoid` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.toList`	—	—

Traversable

Definitions

Name	Category	Theorems
`foldMap` 📖	CompOp	4 math math: `foldMap_hom_free`, `foldMap_map`, `foldMap_hom`, `toList_spec`
`foldl` 📖	CompOp	2 math math: `foldl_map`, `foldl_toList`
`foldlm` 📖	CompOp	2 math math: `foldlm_toList`, `foldlm_map`
`foldr` 📖	CompOp	2 math math: `foldr_toList`, `foldr_map`
`foldrm` 📖	CompOp	2 math math: `foldrm_toList`, `foldrm_map`
`length` 📖	CompOp	1 math math: `length_toList`
`mapFold` 📖	CompOp	—
`toList` 📖	CompOp	8 math math: `foldrm_toList`, `foldr_toList`, `toList_eq_self`, `foldlm_toList`, `foldl_toList`, `length_toList`, `toList_map`, `toList_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`foldMap_hom` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `foldMap` `MulOne.toOne` `MulOne.toMul`	—	`LawfulTraversable.naturality` `instLawfulApplicativeConst`
`foldMap_hom_free` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `FreeMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MonoidHom.instFunLike` `foldMap` `MulOne.toOne` `MulOne.toMul` `FreeMonoid.of`	—	`foldMap_hom`
`foldMap_map` 📖	mathematical	—	`foldMap` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul` `toFunctor`	—	`traverse_map` `instLawfulApplicativeConst`
`foldl_map` 📖	mathematical	—	`foldl` `toFunctor`	—	`foldMap_map`
`foldl_toList` 📖	mathematical	—	`foldl` `toList`	—	`FreeMonoid.toList_ofList` `foldl.unop_ofFreeMonoid` `toList_spec` `foldMap_hom_free`
`foldlm_map` 📖	mathematical	—	`foldlm` `toFunctor`	—	`foldMap_map`
`foldlm_toList` 📖	mathematical	—	`foldlm` `toList`	—	`toList_spec` `foldMap_hom_free` `foldlm.ofFreeMonoid_comp_of`
`foldr_map` 📖	mathematical	—	`foldr` `toFunctor`	—	`foldMap_map`
`foldr_toList` 📖	mathematical	—	`foldr` `toList`	—	`toList_spec` `foldr.eq_1` `Monoid.Foldr.get.eq_1` `FreeMonoid.ofList_toList` `foldMap_hom_free` `foldr.ofFreeMonoid_comp_of`
`foldrm_map` 📖	mathematical	—	`foldrm` `toFunctor`	—	`foldMap_map`
`foldrm_toList` 📖	mathematical	—	`foldrm` `toList`	—	`toList_spec` `foldMap_hom_free` `foldrm.ofFreeMonoid_comp_of`
`length_toList` 📖	mathematical	—	`length` `toList`	—	`foldl_toList` `zero_add`
`toList_eq_self` 📖	mathematical	—	`toList` `instTraversableList`	—	`toList_spec` `List.instLawfulTraversable`
`toList_map` 📖	mathematical	—	`toList` `toFunctor`	—	`toList_spec` `foldMap_map` `foldMap_hom`
`toList_spec` 📖	mathematical	—	`toList` `DFunLike.coe` `Equiv` `FreeMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.toList` `foldMap` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MulOne.toMul` `FreeMonoid.of`	—	`FreeMonoid.reverse_reverse` `foldMap_hom_free`

Traversable.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_eq_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `FreeMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.toList` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MonoidHom.instFunLike` `FreeMonoid.map` `FreeMonoid.ofList`	—	—

Traversable.foldl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_comp_of` 📖	mathematical	—	`FreeMonoid` `Monoid.Foldl` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MulOpposite.instMulOne` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `Monoid.Foldl.ofFreeMonoid` `FreeMonoid.of`	—	—
`unop_ofFreeMonoid` 📖	mathematical	—	`MulOpposite.unop` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `DFunLike.coe` `MonoidHom` `FreeMonoid` `Monoid.Foldl` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MulOpposite.instMulOne` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `Monoid.Foldl.ofFreeMonoid` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `FreeMonoid.toList`	—	—

Traversable.foldlm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_comp_of` 📖	mathematical	—	`FreeMonoid` `Monoid.foldlM` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `MulOpposite.instMulOne` `CategoryTheory.End` `CategoryTheory.KleisliCat` `CategoryTheory.KleisliCat.categoryStruct` `CategoryTheory.End.monoid` `CategoryTheory.KleisliCat.category` `MonoidHom.instFunLike` `Monoid.foldlM.ofFreeMonoid` `FreeMonoid.of`	—	—

Traversable.foldr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_comp_of` 📖	mathematical	—	`FreeMonoid` `Monoid.Foldr` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `CategoryTheory.End.monoid` `CategoryTheory.types` `MonoidHom.instFunLike` `Monoid.Foldr.ofFreeMonoid` `FreeMonoid.of`	—	—

Traversable.foldrm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFreeMonoid_comp_of` 📖	mathematical	—	`FreeMonoid` `Monoid.foldrM` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `FreeMonoid.instCancelMonoid` `CategoryTheory.End.monoid` `CategoryTheory.KleisliCat` `CategoryTheory.KleisliCat.category` `MonoidHom.instFunLike` `Monoid.foldrM.ofFreeMonoid` `FreeMonoid.of`	—	—

---

← Back to Index