Commit 2025-12-05 02:29 a55eb6d1

View on Github →

chore: adaptations for batteries#1490 (#31270) After [batteries#1490](https://github.com/leanprover-community/batteries/pull/1490) 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.finRange_eq_nil
deleted theorem List.finRange_map_get
deleted theorem List.finRange_map_getElem
deleted theorem List.get_finRange
deleted theorem List.map_coe_finRange
deleted theorem List.nodup_finRange
deleted theorem List.pairwise_le_finRange
deleted theorem List.pairwise_lt_finRange