Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-13 18:51 905b875e

View on Github →

chore(data/matrix/block): move block matrices into their own file (#8290) This is a straight cut-and-paste, with no reordering or renaming. Zulip

Estimated changes

deleted theorem matrix.block_diagonal_add
deleted theorem matrix.block_diagonal_mul
deleted theorem matrix.block_diagonal_neg
deleted theorem matrix.block_diagonal_one
deleted theorem matrix.block_diagonal_sub
deleted def matrix.from_blocks
deleted theorem matrix.from_blocks_add
deleted theorem matrix.from_blocks_one
deleted theorem matrix.from_blocks_smul
deleted def matrix.to_block
deleted theorem matrix.to_block_apply
added theorem matrix.from_blocks_add
added theorem matrix.from_blocks_one
added def matrix.to_block
added theorem matrix.to_block_apply