Commit 2024-09-29 04:48 c8df482f

View on Github →

chore: adaptation for batteries#905 (#17229)

Estimated changes

Modified Mathlib/Data/List/Lemmas.lean

deleted theorem List.getElem_tail

Modified lake-manifest.json