Commit 2024-09-03 09:13 b9353a73

View on Github →

chore: move Init.Data.List.Lemmas to Data.List.Defs (#16434)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Defs.lean

added theorem List.length_mapAccumr

added theorem List.length_mapAccumr₂

added def List.mapAccumr

added def List.mapAccumr₂

added theorem List.mem_cons_eq

added theorem List.not_exists_mem_nil

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/Vector/Defs.lean

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

deleted theorem List.length_mapAccumr

deleted theorem List.length_mapAccumr₂

deleted def List.mapAccumr

deleted def List.mapAccumr₂

deleted theorem List.mem_cons_eq

deleted theorem List.not_exists_mem_nil

Modified scripts/noshake.json