mathlib3

5352639d - feat(data/matrix/basic.lean) : added map_scalar and linear_map.map_matrix (#8061)

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. Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>