Documentation Verification Report

AList

📁 Source: Mathlib/Data/Finsupp/AList.lean

Statistics

Metric	Count
Definitions `lookupFinsupp`, `toAList`	2
Theorems `empty_lookupFinsupp`, `insert_lookupFinsupp`, `lookupFinsupp_apply`, `lookupFinsupp_eq_iff_of_ne_zero`, `lookupFinsupp_eq_zero_iff`, `lookupFinsupp_support`, `lookupFinsupp_surjective`, `singleton_lookupFinsupp`, `mem_toAlist`, `toAList_entries`, `toAList_keys_toFinset`, `toAList_lookupFinsupp`	12
Total	14

AList

Definitions

Name	Category	Theorems
`lookupFinsupp` 📖	CompOp	9 math math: `lookupFinsupp_eq_zero_iff`, `lookupFinsupp_eq_iff_of_ne_zero`, `empty_lookupFinsupp`, `lookupFinsupp_support`, `Finsupp.toAList_lookupFinsupp`, `lookupFinsupp_apply`, `lookupFinsupp_surjective`, `singleton_lookupFinsupp`, `insert_lookupFinsupp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_lookupFinsupp` 📖	mathematical	—	`lookupFinsupp` `AList` `instEmptyCollection` `Finsupp` `Finsupp.instZero`	—	—
`insert_lookupFinsupp` 📖	mathematical	—	`lookupFinsupp` `insert` `Finsupp.update`	—	`Finsupp.ext` `lookupFinsupp_apply` `lookup_insert` `Finsupp.coe_update` `Function.update_self` `lookup_insert_ne` `Function.update_of_ne`
`lookupFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `lookupFinsupp` `lookup`	—	—
`lookupFinsupp_eq_iff_of_ne_zero` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `lookupFinsupp` `lookup`	—	`lookupFinsupp_apply`
`lookupFinsupp_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `lookupFinsupp` `AList` `instMembership` `lookup`	—	`lookupFinsupp_apply` `lookup_eq_none`
`lookupFinsupp_support` 📖	mathematical	—	`Finsupp.support` `lookupFinsupp` `List.toFinset` `List.keys` `entries`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`lookupFinsupp_surjective` 📖	mathematical	—	`AList` `Finsupp` `lookupFinsupp`	—	`Finsupp.toAList_lookupFinsupp`
`singleton_lookupFinsupp` 📖	mathematical	—	`lookupFinsupp` `singleton` `Finsupp.single`	—	`insert_lookupFinsupp`

Finsupp

Definitions

Name	Category	Theorems
`toAList` 📖	CompOp	4 math math: `mem_toAlist`, `toAList_entries`, `toAList_lookupFinsupp`, `toAList_keys_toFinset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_toAlist` 📖	mathematical	—	`AList` `AList.instMembership` `toAList`	—	`AList.mem_keys` `List.mem_toFinset` `toAList_keys_toFinset` `mem_support_iff`
`toAList_entries` 📖	mathematical	—	`AList.entries` `toAList` `Prod.toSigma` `Finset.toList` `graph`	—	—
`toAList_keys_toFinset` 📖	mathematical	—	`List.toFinset` `AList.keys` `toAList` `support`	—	`Finset.ext`
`toAList_lookupFinsupp` 📖	mathematical	—	`AList.lookupFinsupp` `toAList`	—	`ext` `AList.lookupFinsupp_apply` `AList.mem_lookup_iff`

---

← Back to Index