GetD
📁 Source: Mathlib/Data/List/GetD.lean
Statistics
List
Definitions
| Name | Category | Theorems |
|---|---|---|
decidableGetDNilNe 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
getD_append 📖 | — | — | — | — | — |
getD_append_right 📖 | — | — | — | — | — |
getD_default_eq_getI 📖 | mathematical | — | getI | — | — |
getD_eq_default 📖 | — | — | — | — | — |
getD_eq_get 📖 | — | — | — | — | getD_eq_getElem |
getD_eq_getD_getElem? 📖 | — | — | — | — | — |
getD_eq_getElem 📖 | — | — | — | — | — |
getD_eq_getElem? 📖 | — | — | — | — | — |
getD_map 📖 | — | — | — | — | — |
getD_replicate 📖 | — | — | — | — | — |
getD_reverse 📖 | — | — | — | — | — |
getD_surjective 📖 | — | — | — | — | getD_surjective_iff |
getD_surjective_iff 📖 | — | — | — | — | — |
getElem?_getD_replicate_default_eq 📖 | — | — | — | — | — |
getElem?_getD_singleton_default_eq 📖 | — | — | — | — | — |
getI_append 📖 | mathematical | — | getI | — | getD_append |
getI_append_right 📖 | mathematical | — | getI | — | getD_append_right |
getI_cons_succ 📖 | mathematical | — | getI | — | — |
getI_cons_zero 📖 | mathematical | — | getI | — | — |
getI_eq_default 📖 | mathematical | — | getI | — | getD_eq_default |
getI_eq_getElem 📖 | mathematical | — | getI | — | getD_eq_getElem |
getI_eq_getElem?_getD 📖 | mathematical | — | getI | — | getD_default_eq_getI |
getI_eq_iget_getElem? 📖 | mathematical | — | getI | — | getI_eq_getElem?_getD |
getI_nil 📖 | mathematical | — | getI | — | — |
getI_zero_eq_headI 📖 | mathematical | — | getIheadI | — | — |
---