Documentation Verification Report

Count

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

Statistics

MetricCount
DefinitionsidxToSigmaCount, sigmaCountToIdx
2
Theoremscoe_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
Total18

List

Definitions

NameCategoryTheorems
idxToSigmaCount 📖CompOp
11 mathmath: 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 mathmath: leftInverse_idxToSigmaCount_sigmaCountToIdx, idxToSigmaCount_sigmaCountToIdx, injective_sigmaCountToIdx, rightInverse_sigmaCountToIdx_idxToSigmaCount, sigmaCountToIdx_idxToSigmaCount, leftInverse_sigmaCountToIdx_idxToSigmaCount, rightInverse_idxToSigmaCount_sigmaCountToIdx, surjective_sigmaCountToIdx, coe_sigmaCountToIdx

Theorems

NameKindAssumesProvesValidatesDepends On
coe_sigmaCountToIdx 📖mathematicalsigmaCountToIdx
idxOfNth
coe_snd_idxToSigmaCount 📖mathematicalidxToSigmaCount
countBefore
count_concat 📖
count_singleton' 📖
fst_idxToSigmaCount 📖mathematicalidxToSigmaCount
idxToSigmaCount_sigmaCountToIdx 📖mathematicalidxToSigmaCount
sigmaCountToIdx
getElem_idxOfNth_eq
injective_idxToSigmaCount 📖mathematicalidxToSigmaCountleftInverse_sigmaCountToIdx_idxToSigmaCount
injective_sigmaCountToIdx 📖mathematicalsigmaCountToIdxleftInverse_idxToSigmaCount_sigmaCountToIdx
leftInverse_idxToSigmaCount_sigmaCountToIdx 📖mathematicalidxToSigmaCount
sigmaCountToIdx
leftInverse_sigmaCountToIdx_idxToSigmaCount 📖mathematicalsigmaCountToIdx
idxToSigmaCount
rightInverse_idxToSigmaCount_sigmaCountToIdx 📖mathematicalidxToSigmaCount
sigmaCountToIdx
rightInverse_sigmaCountToIdx_idxToSigmaCount 📖mathematicalsigmaCountToIdx
idxToSigmaCount
sigmaCountToIdx_idxToSigmaCount 📖mathematicalsigmaCountToIdx
idxToSigmaCount
snd_idxToSigmaCount 📖mathematicalidxToSigmaCount
countBefore
surjective_idxToSigmaCount 📖mathematicalidxToSigmaCountrightInverse_sigmaCountToIdx_idxToSigmaCount
surjective_sigmaCountToIdx 📖mathematicalsigmaCountToIdxrightInverse_idxToSigmaCount_sigmaCountToIdx

---

← Back to Index