Commit 2023-07-30 17:53 2bf4b7ef

View on Github →

feat: port Init.Data.List.Lemmas (#6243)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Init/Data/List/Lemmas.lean

added theorem List.bex_cons

modified theorem List.length_mapAccumr

added theorem List.mem_cons_eq

added theorem List.not_bex_nil