Documentation Verification Report

Sections

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

Statistics

Metric	Count
Definitions `Sections`	1
Theorems `card_sections`, `coe_sections`, `mem_sections`, `sections_add`, `sections_cons`, `sections_zero`	6
Total	7

Multiset

Definitions

Name	Category	Theorems
`Sections` 📖	CompOp	7 math math: `prod_map_sum`, `sections_zero`, `mem_sections`, `sections_cons`, `coe_sections`, `sections_add`, `card_sections`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_sections` 📖	mathematical	—	`card` `Multiset` `Sections` `prod` `Nat.instCommMonoid` `map`	—	`induction_on` `card_singleton` `sections_cons` `card_bind` `map_congr` `card_map` `map_const'` `sum_replicate` `map_cons` `prod_cons`
`coe_sections` 📖	mathematical	—	`Sections` `ofList` `Multiset`	—	`cons_coe` `sections_cons` `bind_map_comm` `coe_bind`
`mem_sections` 📖	mathematical	—	`Multiset` `instMembership` `Sections` `Rel`	—	`induction_on` `sections_cons`
`sections_add` 📖	mathematical	—	`Sections` `Multiset` `instAdd` `bind` `map`	—	`induction_on` `zero_add` `singleton_bind` `map_congr` `map_id'` `cons_add` `sections_cons` `map_bind` `map_map` `bind_assoc` `bind_map`
`sections_cons` 📖	mathematical	—	`Sections` `cons` `Multiset` `bind` `map`	—	`recOn_cons`
`sections_zero` 📖	mathematical	—	`Sections` `Multiset` `instZero` `instSingleton`	—	—

---

← Back to Index