Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `chooseX`, `strongDownwardInduction`, `strongDownwardInductionOn`, `strongInductionOn`, `subsingletonEquiv`, `toList`	6
Theorems `case_strongInductionOn`, `choose_mem`, `choose_property`, `choose_spec`, `coe_subsingletonEquiv`, `coe_toList`, `empty_toList`, `length_toList`, `mem_toList`, `strongDownwardInductionOn_eq`, `strongDownwardInduction_eq`, `strongInductionOn_eq`, `toList_eq_nil`, `toList_eq_singleton_iff`, `toList_singleton`, `toList_zero`	16
Total	22

Multiset

Definitions

Name	Category	Theorems
`chooseX` 📖	CompOp	—
`strongDownwardInduction` 📖	CompOp	1 math math: `strongDownwardInduction_eq`
`strongDownwardInductionOn` 📖	CompOp	1 math math: `strongDownwardInductionOn_eq`
`strongInductionOn` 📖	CompOp	1 math math: `strongInductionOn_eq`
`subsingletonEquiv` 📖	CompOp	1 math math: `coe_subsingletonEquiv`
`toList` 📖	CompOp	12 math math: `coe_toList`, `length_toList`, `prod_toList`, `empty_toList`, `sum_toList`, `toList_eq_singleton_iff`, `mem_toList`, `toList_eq_nil`, `toList_singleton`, `prod_map_toList`, `sum_map_toList`, `toList_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`case_strongInductionOn` 📖	—	`Multiset` `instZero` `cons`	—	—	`induction_on` `lt_of_le_of_lt` `lt_cons_self`
`choose_mem` 📖	mathematical	`ExistsUnique` `Multiset` `instMembership`	`choose`	—	`choose_spec`
`choose_property` 📖	mathematical	`ExistsUnique` `Multiset` `instMembership`	`choose`	—	`choose_spec`
`choose_spec` 📖	mathematical	`ExistsUnique` `Multiset` `instMembership`	`choose`	—	—
`coe_subsingletonEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Multiset` `EquivLike.toFunLike` `Equiv.instEquivLike` `subsingletonEquiv` `ofList`	—	—
`coe_toList` 📖	mathematical	—	`ofList` `toList`	—	`Quotient.out_eq'`
`empty_toList` 📖	mathematical	—	`toList` `Multiset` `instZero`	—	—
`length_toList` 📖	mathematical	—	`toList` `card`	—	`coe_card` `coe_toList`
`mem_toList` 📖	mathematical	—	`toList` `Multiset` `instMembership`	—	`mem_coe` `coe_toList`
`strongDownwardInductionOn_eq` 📖	mathematical	—	`strongDownwardInductionOn`	—	`strongDownwardInduction.eq_1`
`strongDownwardInduction_eq` 📖	mathematical	—	`strongDownwardInduction`	—	`strongDownwardInduction.eq_1`
`strongInductionOn_eq` 📖	mathematical	—	`strongInductionOn`	—	`strongInductionOn.eq_1`
`toList_eq_nil` 📖	mathematical	—	`toList` `Multiset` `instZero`	—	`coe_eq_zero` `coe_toList`
`toList_eq_singleton_iff` 📖	mathematical	—	`toList` `Multiset` `instSingleton`	—	`coe_eq_coe` `coe_toList` `coe_singleton`
`toList_singleton` 📖	mathematical	—	`toList` `Multiset` `instSingleton`	—	`toList_eq_singleton_iff`
`toList_zero` 📖	mathematical	—	`toList` `Multiset` `instZero`	—	`toList_eq_nil`

---

← Back to Index