mathlib

5afd09aa - chore(data/matrix/basic): move bundled versions of `matrix.map` beneath the algebra structure (#8528)

chore(data/matrix/basic): move bundled versions of `matrix.map` beneath the algebra structure (#8528) This will give us an obvious place to add the bundled alg_hom version in a follow-up PR. None of the moved lines have been modified. Note that the git diff shows that instead of `matrix.map` moving down, the `algebra` structure has moved up.