Commit 2024-06-18 08:07 79423dc5

View on Github →

feat(List): Miscellaneous lemmas (#13824) From LeanCamCombi

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.cons_sublist_cons'

added theorem List.getLast_filter

Modified Mathlib/Data/List/Perm.lean

added theorem List.subperm_cons_self