Commit 2024-05-19 22:59 f39480bd

View on Github →

List.rdrop lemmata (#12468) Adds the code from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/List.20lemma.20for.20mathlib

Estimated changes

Modified Mathlib/Data/List/DropRight.lean

added theorem List.rdrop_add

added theorem List.rdrop_append_length

added theorem List.rdrop_append_length_add

added theorem List.rdrop_append_of_le_length

modified theorem List.rtakeWhile_idempotent