Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-19 03:39 fb44330e

View on Github →

feat(data/matrix/block): matrix.block_diagonal is a ring homomorphism (#13489) This is one of the steps on the path to showing that the matrix exponential of a block diagonal matrix is a block diagonal matrix of the exponents of the blocks. As well as adding the new bundled homomorphisms, this generalizes the typeclasses in this file and tidies up the order of arguments. Finally, this protects some map_* lemmas to prevent clashes with the global lemmas of the same name.

Estimated changes

deleted theorem matrix.map_add
deleted theorem matrix.map_sub
deleted theorem matrix.map_zero
modified theorem matrix.block_diagonal'_add
modified theorem matrix.block_diagonal'_map
modified theorem matrix.block_diagonal'_mul
modified theorem matrix.block_diagonal'_neg
modified theorem matrix.block_diagonal'_sub
modified def matrix.block_diagonal
modified theorem matrix.block_diagonal_add
modified theorem matrix.block_diagonal_apply
modified theorem matrix.block_diagonal_map
modified theorem matrix.block_diagonal_mul
modified theorem matrix.block_diagonal_neg
modified theorem matrix.block_diagonal_smul
modified theorem matrix.block_diagonal_sub
modified theorem matrix.from_blocks_add
modified theorem matrix.from_blocks_diagonal
modified theorem matrix.from_blocks_multiply
modified theorem matrix.from_blocks_one
modified theorem matrix.from_blocks_smul