mathlib

4a9cbdb1 - feat(data/matrix/basic): provide equiv versions of `matrix.map`, `linear_map.map_matrix`, and `ring_hom.map_matrix`. (#8468)

feat(data/matrix/basic): provide equiv versions of `matrix.map`, `linear_map.map_matrix`, and `ring_hom.map_matrix`. (#8468) This moves all of these definitions to be adjacent, adds the standard family of functorial simp lemmas, and relaxes some typeclass requirements. This also renames `matrix.one_map` to `matrix.map_one` to match `matrix.map_zero`.