Documentation Verification Report

SplitLengths

📁 Source: Mathlib/Data/List/SplitLengths.lean

Statistics

Metric	Count
Definitions `splitLengths`	1
Theorems `flatten_splitLengths`, `length_mem_splitLengths`, `length_splitLengths`, `length_splitLengths_getElem_eq`, `length_splitLengths_getElem_le`, `map_splitLengths_length`, `splitLengths_cons`, `splitLengths_length_getElem`, `splitLengths_nil`, `take_splitLength`	10
Total	11

List

Definitions

Name	Category	Theorems
`splitLengths` 📖	CompOp	7 math math: `map_splitLengths_length`, `take_splitLength`, `flatten_splitLengths`, `splitLengths_cons`, `length_splitLengths_getElem_eq`, `splitLengths_nil`, `length_splitLengths`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flatten_splitLengths` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	`splitLengths`	—	`splitLengths_cons` `add_comm`
`length_mem_splitLengths` 📖	—	`splitLengths`	—	—	`length_splitLengths_getElem_le` `length_splitLengths`
`length_splitLengths` 📖	mathematical	—	`splitLengths`	—	—
`length_splitLengths_getElem_eq` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	`splitLengths`	—	`take_splitLength` `map_splitLengths_length`
`length_splitLengths_getElem_le` 📖	—	`splitLengths`	—	—	`splitLengths_cons`
`map_splitLengths_length` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	`splitLengths`	—	`splitLengths_cons`
`splitLengths_cons` 📖	mathematical	—	`splitLengths`	—	—
`splitLengths_length_getElem` 📖	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `splitLengths`	—	—	`map_splitLengths_length` `length_splitLengths`
`splitLengths_nil` 📖	mathematical	—	`splitLengths`	—	—
`take_splitLength` 📖	mathematical	—	`splitLengths`	—	`splitLengths_cons`

---

← Back to Index