[Merged by Bors] - chore(Algebra/Module/ZLattice/Summable): automated extraction from #39646#40752

mathlib-splicebot[bot] wants to merge 1 commit into

masterleanprover-community/mathlib4:masterfrom

splice-bot/pr-39646-Mathlib-Algebra-Module-ZLattice-Summable.lean-53400ad9e0-w6o1wvoleanprover-community/mathlib4_copy:splice-bot/pr-39646-Mathlib-Algebra-Module-ZLattice-Summable.lean-53400ad9e0-w6o1wvoCopy head branch name to clipboard