Commit 2023-01-10 15:05 557f77b3

View on Github →

feat: port Data.List.Rdrop (#1382)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Infix.lean

modified theorem List.dropWhile_suffix

modified theorem List.isInfix.filter

modified theorem List.isPrefix.filter

modified theorem List.isSuffix.filter

modified theorem List.takeWhile_prefix

Created Mathlib/Data/List/Rdrop.lean

added theorem List.dropWhile_eq_self_iff

added theorem List.dropWhile_idempotent

added theorem List.mem_rtakeWhile_imp

added def List.rdrop

added def List.rdropWhile

added theorem List.rdropWhile_concat

added theorem List.rdropWhile_concat_neg

added theorem List.rdropWhile_concat_pos

added theorem List.rdropWhile_eq_nil_iff

added theorem List.rdropWhile_eq_self_iff

added theorem List.rdropWhile_last_not

added theorem List.rdropWhile_nil

added theorem List.rdropWhile_prefix

added theorem List.rdropWhile_singleton

added theorem List.rdrop_concat_succ

added theorem List.rdrop_eq_reverse_drop_reverse

added theorem List.rdrop_nil

added theorem List.rdrop_while_idempotent

added theorem List.rdrop_zero

added def List.rtake

added def List.rtakeWhile

added theorem List.rtakeWhile_concat

added theorem List.rtakeWhile_concat_neg

added theorem List.rtakeWhile_concat_pos

added theorem List.rtakeWhile_eq_nil_iff

added theorem List.rtakeWhile_eq_self_iff

added theorem List.rtakeWhile_idempotent

added theorem List.rtakeWhile_nil

added theorem List.rtakeWhile_suffix

added theorem List.rtake_concat_succ

added theorem List.rtake_eq_reverse_take_reverse

added theorem List.rtake_nil

added theorem List.rtake_zero