Theorem ContinuousLinearEquiv.tsum_eq_iff

Modification history

2023-04-05 08:46
Mathlib/Topology/Algebra/InfiniteSum/Module.lean
feat: port Topology.Algebra.InfiniteSum.Module (#3272)
Added ContinuousLinearEquiv.tsum_eq_iffView on Github →