Commit 2024-11-26 22:19 21af8545

View on Github →

chore: adaptation to batteries#1055 (#19487)

Estimated changes

Modified Mathlib/Data/Fin/VecNotation.lean

Modified Mathlib/Data/List/Defs.lean

deleted def List.finRange

Modified Mathlib/Data/List/FinRange.lean

deleted theorem List.finRange_succ

deleted theorem List.finRange_zero

deleted theorem List.getElem_finRange

deleted theorem List.length_finRange

Modified Mathlib/ModelTheory/Encoding.lean

Modified lake-manifest.json

Modified lakefile.lean