Scan

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

Statistics

Metric	Count
Definitions	0
Theorems getElem?_partialProds, getElem?_partialSums, getElem_flatten, getElem_flatten_aux₁, getElem_flatten_aux₂, getElem_partialProds, getElem_partialSums, length_flatten_mem_partialSums_map_length, length_partialProds, length_partialSums, partialProds_append, partialProds_cons, partialProds_nil, partialSums_append, partialSums_cons, partialSums_ne_nil, partialSums_nil, take_partialProds, take_partialSums	19
Total	19

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
getElem?_partialProds 📖	mathematical	—	partialProds prod	—	—
getElem?_partialSums 📖	mathematical	—	partialSums	—	—
getElem_flatten 📖	—	—	—	—	getElem_flatten_aux₁ getElem_flatten_aux₂ partialSums_cons getElem_partialSums length_partialSums
getElem_flatten_aux₁ 📖	mathematical	—	partialSums	—	getElem_partialSums length_partialSums length_flatten_mem_partialSums_map_length
getElem_flatten_aux₂ 📖	mathematical	—	partialSums getElem_flatten_aux₁	—	getElem_flatten_aux₁ partialSums_cons length_partialSums getElem_partialSums
getElem_partialProds 📖	mathematical	partialProds	partialProds prod	—	prod_eq_foldl
getElem_partialSums 📖	mathematical	partialSums	partialSums	—	sum_eq_foldl
length_flatten_mem_partialSums_map_length 📖	mathematical	—	partialSums	—	partialSums_nil partialSums_cons
length_partialProds 📖	mathematical	—	partialProds	—	—
length_partialSums 📖	mathematical	—	partialSums	—	—
partialProds_append 📖	mathematical	—	partialProds prod	—	partialProds_cons
partialProds_cons 📖	mathematical	—	partialProds	—	—
partialProds_nil 📖	mathematical	—	partialProds	—	—
partialSums_append 📖	mathematical	—	partialSums	—	partialSums_cons
partialSums_cons 📖	mathematical	—	partialSums	—	—
partialSums_ne_nil 📖	—	—	—	—	length_partialSums
partialSums_nil 📖	mathematical	—	partialSums	—	—
take_partialProds 📖	mathematical	—	partialProds	—	—
take_partialSums 📖	mathematical	—	partialSums	—	—

---

← Back to Index