Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.algebra_map_eq_diagonal_ring_hom

Modification history

2021-08-05 16:28
src/data/matrix/basic.lean
feat(data/matrix/basic): add `alg_(hom|equiv).map_matrix` (#8527) …
Added matrix.algebra_map_eq_diagonal_ring_homView on Github →