Flatten

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

Statistics

Metric	Count
Definitions	0
Theorems flatMap, flatMap_right, flatten, append_flatten_map_append, drop_take_succ_eq_cons_getElem, getLast_flatten_eq_getLast_getLast, getLast_flatten_of_flatten_ne_nil, getLast_flatten_of_getLast_ne_nil, getLast_getLast_eq_getLast_flatten, head_flatten_eq_head_head, head_head_eq_head_flatten	11
Total	11

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append_flatten_map_append 📖	—	—	—	—	—
drop_take_succ_eq_cons_getElem 📖	—	—	—	—	—
getLast_flatten_eq_getLast_getLast 📖	—	—	—	—	getLast_getLast_eq_getLast_flatten
getLast_flatten_of_flatten_ne_nil 📖	—	—	—	—	getLast_flatten_eq_getLast_getLast
getLast_flatten_of_getLast_ne_nil 📖	—	—	—	—	getLast_getLast_eq_getLast_flatten
getLast_getLast_eq_getLast_flatten 📖	—	—	—	—	—
head_flatten_eq_head_head 📖	—	—	—	—	head_head_eq_head_flatten
head_head_eq_head_flatten 📖	—	—	—	—	—

List.Sublist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flatMap 📖	—	—	—	—	flatten
flatMap_right 📖	—	—	—	—	—
flatten 📖	—	—	—	—	—

---

← Back to Index