Commit 2021-06-24 11:32 5352639d
View on Github →feat(data/matrix/basic.lean) : added map_scalar and linear_map.map_matrix (#8061)
Added two lemmas (map_scalar and linear_map.map_matrix_apply) and a definition (linear_map.map_matrix) showing that a map between coefficients induces the same type of map between matrices with those coefficients.