Documentation Verification Report

Count

📁 Source: Batteries/Data/List/Count.lean

Statistics

Metric	Count
Definitions `idxToSigmaCount`, `sigmaCountToIdx`	2
Theorems `coe_sigmaCountToIdx`, `coe_snd_idxToSigmaCount`, `count_concat`, `count_singleton'`, `fst_idxToSigmaCount`, `idxToSigmaCount_sigmaCountToIdx`, `injective_idxToSigmaCount`, `injective_sigmaCountToIdx`, `leftInverse_idxToSigmaCount_sigmaCountToIdx`, `leftInverse_sigmaCountToIdx_idxToSigmaCount`, `rightInverse_idxToSigmaCount_sigmaCountToIdx`, `rightInverse_sigmaCountToIdx_idxToSigmaCount`, `sigmaCountToIdx_idxToSigmaCount`, `snd_idxToSigmaCount`, `surjective_idxToSigmaCount`, `surjective_sigmaCountToIdx`	16
Total	18

List

Definitions

Name	Category	Theorems
`idxToSigmaCount` 📖	CompOp	11 math math: `leftInverse_idxToSigmaCount_sigmaCountToIdx`, `snd_idxToSigmaCount`, `injective_idxToSigmaCount`, `idxToSigmaCount_sigmaCountToIdx`, `rightInverse_sigmaCountToIdx_idxToSigmaCount`, `sigmaCountToIdx_idxToSigmaCount`, `leftInverse_sigmaCountToIdx_idxToSigmaCount`, `fst_idxToSigmaCount`, `surjective_idxToSigmaCount`, `rightInverse_idxToSigmaCount_sigmaCountToIdx`, `coe_snd_idxToSigmaCount`
`sigmaCountToIdx` 📖	CompOp	9 math math: `leftInverse_idxToSigmaCount_sigmaCountToIdx`, `idxToSigmaCount_sigmaCountToIdx`, `injective_sigmaCountToIdx`, `rightInverse_sigmaCountToIdx_idxToSigmaCount`, `sigmaCountToIdx_idxToSigmaCount`, `leftInverse_sigmaCountToIdx_idxToSigmaCount`, `rightInverse_idxToSigmaCount_sigmaCountToIdx`, `surjective_sigmaCountToIdx`, `coe_sigmaCountToIdx`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_sigmaCountToIdx` 📖	mathematical	—	`sigmaCountToIdx` `idxOfNth`	—	—
`coe_snd_idxToSigmaCount` 📖	mathematical	—	`idxToSigmaCount` `countBefore`	—	—
`count_concat` 📖	—	—	—	—	—
`count_singleton'` 📖	—	—	—	—	—
`fst_idxToSigmaCount` 📖	mathematical	—	`idxToSigmaCount`	—	—
`idxToSigmaCount_sigmaCountToIdx` 📖	mathematical	—	`idxToSigmaCount` `sigmaCountToIdx`	—	`getElem_idxOfNth_eq`
`injective_idxToSigmaCount` 📖	mathematical	—	`idxToSigmaCount`	—	`leftInverse_sigmaCountToIdx_idxToSigmaCount`
`injective_sigmaCountToIdx` 📖	mathematical	—	`sigmaCountToIdx`	—	`leftInverse_idxToSigmaCount_sigmaCountToIdx`
`leftInverse_idxToSigmaCount_sigmaCountToIdx` 📖	mathematical	—	`idxToSigmaCount` `sigmaCountToIdx`	—	—
`leftInverse_sigmaCountToIdx_idxToSigmaCount` 📖	mathematical	—	`sigmaCountToIdx` `idxToSigmaCount`	—	—
`rightInverse_idxToSigmaCount_sigmaCountToIdx` 📖	mathematical	—	`idxToSigmaCount` `sigmaCountToIdx`	—	—
`rightInverse_sigmaCountToIdx_idxToSigmaCount` 📖	mathematical	—	`sigmaCountToIdx` `idxToSigmaCount`	—	—
`sigmaCountToIdx_idxToSigmaCount` 📖	mathematical	—	`sigmaCountToIdx` `idxToSigmaCount`	—	—
`snd_idxToSigmaCount` 📖	mathematical	—	`idxToSigmaCount` `countBefore`	—	—
`surjective_idxToSigmaCount` 📖	mathematical	—	`idxToSigmaCount`	—	`rightInverse_sigmaCountToIdx_idxToSigmaCount`
`surjective_sigmaCountToIdx` 📖	mathematical	—	`sigmaCountToIdx`	—	`rightInverse_idxToSigmaCount_sigmaCountToIdx`

---

← Back to Index