Theorem Summable.smul_const

Modification history

2024-02-29 08:53

Mathlib/Topology/Algebra/InfiniteSum/Module.lean

chore(Topology/Algebra/InfiniteSum): split up large file (#11050) …

Modified Summable.smul_const View on Github →

2023-04-05 08:46

Mathlib/Topology/Algebra/InfiniteSum/Module.lean

feat: port Topology.Algebra.InfiniteSum.Module (#3272)

Added Summable.smul_const View on Github →