Commit 2022-07-13 21:11 4302cb7e

View on Github →

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

Estimated changes

Modified src/data/matrix/block.lean

added theorem matrix.from_blocks_minor_sum_swap_left

added theorem matrix.from_blocks_minor_sum_swap_right

added theorem matrix.from_blocks_minor_sum_swap_sum_swap

Modified src/logic/equiv/basic.lean