Commit 2021-08-02 20:14 17f1d28c

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.