Documentation Verification Report

SplitBy

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

Statistics

MetricCount
Definitions0
Theoremschain'_getLast_head_splitBy, chain'_of_mem_splitBy, flatten_splitBy, getLast_getLast_splitBy, head_head_splitBy, isChain_getLast_head_splitBy, isChain_of_mem_splitBy, ne_nil_of_mem_splitBy, nil_notMem_splitBy, splitBy_append, splitBy_append_cons, splitBy_eq_iff, splitBy_eq_nil, splitBy_flatten, splitBy_ne_nil, splitBy_nil, splitBy_of_isChain
17
Total17

List

Theorems

NameKindAssumesProvesValidatesDepends On
chain'_getLast_head_splitBy 📖isChain_getLast_head_splitBy
chain'_of_mem_splitBy 📖isChain_of_mem_splitBy
flatten_splitBy 📖
getLast_getLast_splitBy 📖mathematicalsplitBy_ne_nil
ne_nil_of_mem_splitBy
splitBy_ne_nil
ne_nil_of_mem_splitBy
flatten_splitBy
getLast_getLast_eq_getLast_flatten
head_head_splitBy 📖mathematicalsplitBy_ne_nil
ne_nil_of_mem_splitBy
splitBy_ne_nil
ne_nil_of_mem_splitBy
flatten_splitBy
head_head_eq_head_flatten
isChain_getLast_head_splitBy 📖isChain_nil
isChain_of_mem_splitBy 📖instIsEmptyFalse
ne_nil_of_mem_splitBy 📖
nil_notMem_splitBy 📖
splitBy_append 📖eq_or_ne
splitBy_eq_iff
flatten_splitBy
isChain_of_mem_splitBy
isChain_append
isChain_getLast_head_splitBy
ne_nil_of_mem_splitBy
getLast_getLast_splitBy
head_head_splitBy
splitBy_append_cons 📖splitBy_append
splitBy_eq_iff 📖flatten_splitBy
nil_notMem_splitBy
isChain_of_mem_splitBy
isChain_getLast_head_splitBy
splitBy_flatten
splitBy_eq_nil 📖flatten_splitBy
splitBy_flatten 📖isChain_cons
head_flatten_eq_head_head
IsChain.tail
splitBy_ne_nil 📖Iff.not
splitBy_eq_nil
splitBy_nil 📖
splitBy_of_isChain 📖splitBy.eq_2
instIsEmptyFalse

---

← Back to Index