DropRight

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

Statistics

Metric	Count
Definitions `rdrop`, `rdropWhile`, `rtake`, `rtakeWhile`	4
Theorems `dropWhile_idempotent`, `mem_rtakeWhile_imp`, `rdropWhile_append_rtakeWhile`, `rdropWhile_concat`, `rdropWhile_concat_neg`, `rdropWhile_concat_pos`, `rdropWhile_eq_nil_iff`, `rdropWhile_eq_self_iff`, `rdropWhile_idempotent`, `rdropWhile_last_not`, `rdropWhile_nil`, `rdropWhile_prefix`, `rdropWhile_reverse`, `rdropWhile_singleton`, `rdrop_add`, `rdrop_append_length`, `rdrop_append_length_add`, `rdrop_append_of_le_length`, `rdrop_concat_succ`, `rdrop_eq_reverse_drop_reverse`, `rdrop_nil`, `rdrop_zero`, `rtakeWhile_concat`, `rtakeWhile_concat_neg`, `rtakeWhile_concat_pos`, `rtakeWhile_eq_nil_iff`, `rtakeWhile_eq_self_iff`, `rtakeWhile_idempotent`, `rtakeWhile_nil`, `rtakeWhile_reverse`, `rtakeWhile_suffix`, `rtake_concat_succ`, `rtake_eq_reverse_take_reverse`, `rtake_nil`, `rtake_zero`	35
Total	39

List

Definitions

Name	Category	Theorems
`rdrop` 📖	CompOp	8 math math: `rdrop_append_length`, `rdrop_concat_succ`, `rdrop_eq_reverse_drop_reverse`, `rdrop_add`, `rdrop_append_of_le_length`, `rdrop_zero`, `rdrop_append_length_add`, `rdrop_nil`
`rdropWhile` 📖	CompOp	12 math math: `rdropWhile_singleton`, `rdropWhile_last_not`, `rdropWhile_reverse`, `rdropWhile_idempotent`, `rdropWhile_nil`, `rdropWhile_eq_nil_iff`, `rdropWhile_concat_pos`, `rdropWhile_prefix`, `rdropWhile_eq_self_iff`, `rdropWhile_append_rtakeWhile`, `rdropWhile_concat_neg`, `rdropWhile_concat`
`rtake` 📖	CompOp	4 math math: `rtake_eq_reverse_take_reverse`, `rtake_zero`, `rtake_concat_succ`, `rtake_nil`
`rtakeWhile` 📖	CompOp	10 math math: `rtakeWhile_eq_nil_iff`, `rtakeWhile_reverse`, `rtakeWhile_idempotent`, `rtakeWhile_concat_neg`, `rtakeWhile_suffix`, `rtakeWhile_concat_pos`, `rtakeWhile_concat`, `rtakeWhile_nil`, `rdropWhile_append_rtakeWhile`, `rtakeWhile_eq_self_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dropWhile_idempotent` 📖	—	—	—	—	`dropWhile_get_zero_not`
`mem_rtakeWhile_imp` 📖	—	`rtakeWhile`	—	—	`mem_takeWhile_imp` `rtakeWhile.eq_1`
`rdropWhile_append_rtakeWhile` 📖	mathematical	—	`rdropWhile` `rtakeWhile`	—	—
`rdropWhile_concat` 📖	mathematical	—	`rdropWhile`	—	—
`rdropWhile_concat_neg` 📖	mathematical	—	`rdropWhile`	—	`rdropWhile_concat`
`rdropWhile_concat_pos` 📖	mathematical	—	`rdropWhile`	—	`rdropWhile_concat`
`rdropWhile_eq_nil_iff` 📖	mathematical	—	`rdropWhile`	—	—
`rdropWhile_eq_self_iff` 📖	mathematical	—	`rdropWhile`	—	—
`rdropWhile_idempotent` 📖	mathematical	—	`rdropWhile`	—	`rdropWhile_eq_self_iff` `rdropWhile_last_not`
`rdropWhile_last_not` 📖	mathematical	—	`rdropWhile`	—	—
`rdropWhile_nil` 📖	mathematical	—	`rdropWhile`	—	—
`rdropWhile_prefix` 📖	mathematical	—	`rdropWhile`	—	`rdropWhile.eq_1`
`rdropWhile_reverse` 📖	mathematical	—	`rdropWhile`	—	—
`rdropWhile_singleton` 📖	mathematical	—	`rdropWhile`	—	`rdropWhile_concat` `rdropWhile_nil`
`rdrop_add` 📖	mathematical	—	`rdrop`	—	`rdrop_eq_reverse_drop_reverse`
`rdrop_append_length` 📖	mathematical	—	`rdrop`	—	`rdrop_eq_reverse_drop_reverse`
`rdrop_append_length_add` 📖	mathematical	—	`rdrop`	—	`rdrop_add` `rdrop_append_length`
`rdrop_append_of_le_length` 📖	mathematical	—	`rdrop`	—	`rdrop_eq_reverse_drop_reverse`
`rdrop_concat_succ` 📖	mathematical	—	`rdrop`	—	`rdrop_eq_reverse_drop_reverse`
`rdrop_eq_reverse_drop_reverse` 📖	mathematical	—	`rdrop`	—	`rdrop.eq_1`
`rdrop_nil` 📖	mathematical	—	`rdrop`	—	—
`rdrop_zero` 📖	mathematical	—	`rdrop`	—	—
`rtakeWhile_concat` 📖	mathematical	—	`rtakeWhile`	—	—
`rtakeWhile_concat_neg` 📖	mathematical	—	`rtakeWhile`	—	`rtakeWhile_concat`
`rtakeWhile_concat_pos` 📖	mathematical	—	`rtakeWhile`	—	`rtakeWhile_concat`
`rtakeWhile_eq_nil_iff` 📖	mathematical	—	`rtakeWhile`	—	`instIsEmptyFalse`
`rtakeWhile_eq_self_iff` 📖	mathematical	—	`rtakeWhile`	—	—
`rtakeWhile_idempotent` 📖	mathematical	—	`rtakeWhile`	—	`rtakeWhile_eq_self_iff` `mem_rtakeWhile_imp`
`rtakeWhile_nil` 📖	mathematical	—	`rtakeWhile`	—	—
`rtakeWhile_reverse` 📖	mathematical	—	`rtakeWhile`	—	—
`rtakeWhile_suffix` 📖	mathematical	—	`rtakeWhile`	—	`rtakeWhile.eq_1`
`rtake_concat_succ` 📖	mathematical	—	`rtake`	—	`rtake_eq_reverse_take_reverse`
`rtake_eq_reverse_take_reverse` 📖	mathematical	—	`rtake`	—	`rtake.eq_1`
`rtake_nil` 📖	mathematical	—	`rtake`	—	—
`rtake_zero` 📖	mathematical	—	`rtake`	—	—

---

← Back to Index