mathlib

17f1d28c - chore(data/matrix): delete each of the `matrix.foo_hom_map_zero` (#8512)

chore(data/matrix): delete each of the `matrix.foo_hom_map_zero` (#8512) These can already be found by `simp` since `matrix.map_zero` is a `simp` lemma, and we can manually use `foo_hom.map_matrix.map_zero` introduced by #8468 instead. They also don't seem to be used anywhere in mathlib, given that deleting them with no replacement causes no build errors. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>