Commit 2024-11-13 19:26 d2aa4352

View on Github →

feat(Data/List/Basic): lemmas relating find? to head of dropWhile (#18473) Add lemmas relating the result of List.find? to that of List.head? or List.head on List.dropWhile.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.find?_eq_head?_dropWhile_not

added theorem List.find?_eq_head_dropWhile_not

added theorem List.find?_not_eq_head?_dropWhile

added theorem List.find?_not_eq_head_dropWhile