Commit 2025-06-05 23:26 6437a626

View on Github →

chore: update batteries dependency (including fixes for batteries#1220) (#25478)

Estimated changes

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

Modified Mathlib/Algebra/BigOperators/Group/Finset/Preimage.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Algebra/Group/Submonoid/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/NeZero.lean

Modified Mathlib/Algebra/Homology/DifferentialObject.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean

added theorem WeierstrassCurve.Affine.slope_of_Y_ne'

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean

modified theorem ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/Data/Finset/Fold.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Int/Init.lean

modified theorem Int.toNat_pred_coe_of_pos

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Set/Function.lean

added theorem Set.injOn_of_eq_iff_eq

Modified Mathlib/Data/Vector/MapLemmas.lean

modified theorem List.Vector.mapAccumr_eq_map_of_unused_state

modified theorem List.Vector.mapAccumr₂_eq_map₂_of_unused_state

modified theorem List.Vector.mapAccumr₂_unused_input_left

modified theorem List.Vector.mapAccumr₂_unused_input_right

Modified Mathlib/Data/ZMod/Basic.lean

modified theorem nsmul_zmod_val_inv_nsmul

modified theorem pow_pow_zmod_val_inv

modified theorem pow_zmod_val_inv_pow

modified theorem zmod_val_inv_nsmul_nsmul

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

Modified lake-manifest.json