Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-05 16:28 8e79ea53

View on Github →

feat(data/matrix/basic): add alg_(hom|equiv).map_matrix (#8527) This also adds a few standalone lemmas about algebra_map.

Estimated changes

Modified src/data/matrix/basic.lean

added def alg_equiv.map_matrix

added theorem alg_equiv.map_matrix_refl

added theorem alg_equiv.map_matrix_symm

added theorem alg_equiv.map_matrix_trans

added def alg_hom.map_matrix

added theorem alg_hom.map_matrix_comp

added theorem alg_hom.map_matrix_id

added theorem matrix.algebra_map_eq_diagonal

added theorem matrix.algebra_map_eq_diagonal_ring_hom

added theorem matrix.map_algebra_map