Commit 2022-04-29 12:25 8eb25641

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.