Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alg_equiv.map_matrix_trans

Modification history

2021-08-05 16:28

src/data/matrix/basic.lean

feat(data/matrix/basic): add `alg_(hom|equiv).map_matrix` (#8527) …

Added alg_equiv.map_matrix_trans View on Github →