Commit 2023-09-29 15:19 071f47d2

View on Github →

feat: add some List.takeWhile lemmas (#7397)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.takeWhile_cons

added theorem List.takeWhile_cons_of_neg

added theorem List.takeWhile_cons_of_pos

added theorem List.takeWhile_nil