block): lemmas about swapping blocks of matrices (#15298)

Commit

3 years ago

chore(data/matrix/block): lemmas about swapping blocks of matrices (#15298) Also makes `equiv.sum_comm` reduce to `equiv.sum_swap` slightly more agressively.

Author

eric-wieser

Parents

5590b0a2

mathlib 4302cb7e - chore(data/matrix/block): lemmas about swapping blocks of matrices (#15298)

mathlib
4302cb7e - chore(data/matrix/block): lemmas about swapping blocks of matrices (#15298)