Commit 2025-11-16 12:52 1fb8d955

View on Github →

chore: adaptations for batteries#1486 (#31182) After [batteries#1486](https://github.com/leanprover-community/batteries/pull/1486) 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

Modified Mathlib/Algebra/BigOperators/Group/List/Basic.lean

deleted theorem List.prod_append

deleted theorem List.prod_concat

deleted theorem List.prod_eq_foldl

deleted theorem List.prod_flatten

Modified Mathlib/Algebra/BigOperators/Group/List/Defs.lean

deleted def List.prod

deleted theorem List.prod_cons

deleted theorem List.prod_eq_foldr

deleted theorem List.prod_nil

deleted theorem List.prod_one_cons

deleted theorem List.prod_singleton

Modified Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Order/BigOperators/Ring/List.lean

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

modified theorem Polynomial.subsingleton_isRoot_of_natDegree_eq_one

Modified Mathlib/Algebra/Polynomial/Div.lean

modified theorem Irreducible.subsingleton_isRoot

Modified Mathlib/Data/List/Prime.lean

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

modified theorem FreeGroup.lift_apply_of

Modified MathlibTest/LibraryRewrite.lean

Modified lake-manifest.json

Modified scripts/noshake.json