mathlib

8eb25641 - feat(topology/instances/matrix): add `matrix` lemmas about `tsum` (#13677)

feat(topology/instances/matrix): add `matrix` lemmas about `tsum` (#13677) This adds lemmas about how `tsum` interacts with `diagonal` and `transpose`, along with the helper `summable` and `has_sum` lemmas. This also moves `topology/algebra/matrix` to `topology/instances/matrix`, since that seems to align better with how other types are handled.