Documentation Verification Report

Functor

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

Statistics

Metric	Count
Definitions `functor`, `instMonad`, `traverse`	3
Theorems `bind_def`, `comp_traverse`, `fmap_def`, `id_traverse`, `instLawfulFunctor`, `instLawfulMonad`, `map_comp_coe`, `map_traverse`, `naturality`, `pure_def`, `traverse_map`	11
Total	14

Multiset

Definitions

Name	Category	Theorems
`functor` 📖	CompOp	6 math math: `fmap_def`, `Finset.map_comp_coe_apply`, `instLawfulFunctor`, `Finset.map_comp_coe`, `map_traverse`, `map_comp_coe`
`instMonad` 📖	CompOp	3 math math: `bind_def`, `pure_def`, `instLawfulMonad`
`traverse` 📖	CompOp	5 math math: `id_traverse`, `comp_traverse`, `map_traverse`, `naturality`, `traverse_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_def` 📖	mathematical	—	`Multiset` `instMonad` `bind`	—	—
`comp_traverse` 📖	mathematical	—	`traverse` `Functor.Comp` `Functor.Comp.instApplicativeComp` `Functor.Comp.instCommApplicative` `Multiset`	—	`Functor.Comp.instCommApplicative` `Traversable.traverse_comp` `List.instLawfulTraversable` `CommApplicative.toLawfulApplicative` `lift_coe`
`fmap_def` 📖	mathematical	—	`Multiset` `functor` `map`	—	—
`id_traverse` 📖	mathematical	—	`traverse` `instCommApplicativeId` `Multiset`	—	`instCommApplicativeId` `lift_coe` `LawfulTraversable.id_traverse` `List.instLawfulTraversable` `CommApplicative.toLawfulApplicative`
`instLawfulFunctor` 📖	mathematical	—	`Multiset` `functor`	—	`map_congr` `map_id'` `map_map`
`instLawfulMonad` 📖	mathematical	—	`Multiset` `instMonad`	—	`map_congr` `map_id'` `singleton_bind` `bind_assoc` `bind_singleton`
`map_comp_coe` 📖	mathematical	—	`Multiset` `functor` `ofList`	—	—
`map_traverse` 📖	mathematical	—	`Multiset` `functor` `traverse`	—	`lift_coe` `CommApplicative.toLawfulApplicative` `Traversable.map_traverse'` `List.instLawfulTraversable`
`naturality` 📖	mathematical	—	`Multiset` `traverse`	—	`lift_coe` `ApplicativeTransformation.preserves_map` `CommApplicative.toLawfulApplicative` `LawfulTraversable.naturality` `List.instLawfulTraversable`
`pure_def` 📖	mathematical	—	`Multiset` `instMonad` `instSingleton`	—	—
`traverse_map` 📖	mathematical	—	`traverse` `map`	—	`lift_coe` `Traversable.traverse_map` `List.instLawfulTraversable` `CommApplicative.toLawfulApplicative` `List.map_eq_map`

---

← Back to Index