Commit 2025-11-25 00:00 7bf950c8

View on Github →

chore: adaptation for batteries#1500 (#32075) After [batteries#1500](https://github.com/leanprover-community/batteries/pull/1500) is merged:

  • Edit the lakefile to point to leanprover-community/batteries:main
  • Run lake update batteries
  • Merge leanprover-community/mathlib4:master
  • Wait for CI and merge

Estimated changes

deleted theorem List.getElem_idxOf
modified theorem List.get_idxOf
modified theorem List.idxOf_getElem