Commit 2023-04-05 08:46 2461fc6b

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/InfiniteSum/Module.lean

added theorem ContinuousLinearEquiv.tsum_eq_iff

added theorem HasSum.smul_const

added theorem Summable.smul_const

added theorem tsum_smul_const