mathlib

fb44330e - feat(data/matrix/block): `matrix.block_diagonal` is a ring homomorphism (#13489)

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.