Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.block_diagonal'_conj_transpose

Modification history

2022-04-19 03:39
src/data/matrix/block.lean
feat(data/matrix/block): `matrix.block_diagonal` is a ring homomorphism (#13489) …
Modified matrix.block_diagonal'_conj_transposeView on Github →
2021-07-15 16:32
src/data/matrix/block.lean
feat(data/matrix/{basic, block}): missing lemmas on conj_transpose (#8303) …
Added matrix.block_diagonal'_conj_transposeView on Github →