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>

src/data/matrix/basic.lean

@@ -468,84 +468,6 @@ instance [decidable_eq n] : semiring (matrix n n α) :=
 
 end semiring
 
-section homs
-
--- TODO: there should be a way to avoid restating these for each `foo_hom`.
-/-- A version of `map_one` where `f` is a ring hom. -/
-@[simp] lemma ring_hom_map_one [decidable_eq n] [semiring α] [semiring β] (f : α →+* β) :
-  (1 : matrix n n α).map f = 1 :=
-map_one _ f.map_zero f.map_one
-
-/-- A version of `map_one` where `f` is a `ring_equiv`. -/
-@[simp] lemma ring_equiv_map_one [decidable_eq n]  [semiring α] [semiring β] (f : α ≃+* β) :
-  (1 : matrix n n α).map f = 1 :=
-map_one _ f.map_zero f.map_one
-
-/-- A version of `map_zero` where `f` is a `zero_hom`. -/
-@[simp] lemma zero_hom_map_zero [has_zero α] [has_zero β] (f : zero_hom α β) :
-  (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `map_zero` where `f` is a `add_monoid_hom`. -/
-@[simp] lemma add_monoid_hom_map_zero [add_monoid α] [add_monoid β] (f : α →+ β) :
-  (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `map_zero` where `f` is a `add_equiv`. -/
-@[simp] lemma add_equiv_map_zero [add_monoid α] [add_monoid β] (f : α ≃+ β) :
-  (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `map_zero` where `f` is a `linear_map`. -/
-@[simp] lemma linear_map_map_zero [semiring R] [add_comm_monoid α] [add_comm_monoid β]
-  [module R α] [module R β] (f : α →ₗ[R] β) :
-  (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `map_zero` where `f` is a `linear_equiv`. -/
-@[simp] lemma linear_equiv_map_zero [semiring R] [add_comm_monoid α] [add_comm_monoid β]
-  [module R α] [module R β] (f : α ≃ₗ[R] β) :
-  (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `map_zero` where `f` is a `ring_hom`. -/
-@[simp] lemma ring_hom_map_zero [semiring α] [semiring β] (f : α →+* β) :
-  (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `map_zero` where `f` is a `ring_equiv`. -/
-@[simp] lemma ring_equiv_map_zero [semiring α] [semiring β] (f : α ≃+* β) :
-  (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-section algebra
-
-variables [comm_semiring R] [semiring α] [algebra R α] [semiring β] [algebra R β]
-
-/-- A version of `matrix.map_one` where `f` is an `alg_hom`. -/
-@[simp] lemma alg_hom_map_one [decidable_eq n]
-  (f : α →ₐ[R] β) : (1 : matrix n n α).map f = 1 :=
-map_one _ f.map_zero f.map_one
-
-/-- A version of `matrix.map_one` where `f` is an `alg_equiv`. -/
-@[simp] lemma alg_equiv_map_one [decidable_eq n]
-  (f : α ≃ₐ[R] β) : (1 : matrix n n α).map f = 1 :=
-map_one _ f.map_zero f.map_one
-
-/-- A version of `matrix.zero_map` where `f` is an `alg_hom`. -/
-@[simp] lemma alg_hom_map_zero
-  (f : α →ₐ[R] β) : (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `matrix.zero_map` where `f` is an `alg_equiv`. -/
-@[simp] lemma alg_equiv_map_zero
-  (f : α ≃ₐ[R] β) : (0 : matrix n n α).map f = 0 :=
-map_zero _ f.map_zero
-
-end algebra
-
-end homs
-
 end matrix
 
 /-!