chore(linear_algebra/matrix/hermitian): move matrix.conj_transpose_map to the same file as matrix.transpose_map (#15297)

Also restates the hypothesis using `function.semiconj` since that has more API and is definitionally easier to work with.

Author: eric-wieser

src/data/matrix/basic.lean

@@ -1515,6 +1515,11 @@ matrix.ext $ by simp [mul_apply]
   (- M)ᴴ = - Mᴴ :=
 matrix.ext $ by simp
 
+lemma conj_transpose_map [has_star α] [has_star β] {A : matrix m n α} (f : α → β)
+  (hf : function.semiconj f star star) :
+  Aᴴ.map f = (A.map f)ᴴ :=
+matrix.ext $ λ i j, hf _
+
 /-- `matrix.conj_transpose` as an `add_equiv` -/
 @[simps apply]
 def conj_transpose_add_equiv [add_monoid α] [star_add_monoid α] : matrix m n α ≃+ matrix n m α :=

src/linear_algebra/matrix/hermitian.lean

@@ -67,23 +67,18 @@ by simp [is_hermitian, add_comm]
   (0 : matrix n n α).is_hermitian :=
 conj_transpose_zero
 
--- TODO: move
-lemma conj_transpose_map {A : matrix n n α} (f : α → β) (hf : f ∘ star = star ∘ f) :
-  Aᴴ.map f = (A.map f)ᴴ :=
-by rw [conj_transpose, conj_transpose, ←transpose_map, map_map, map_map, hf]
-
 @[simp] lemma is_hermitian.map {A : matrix n n α} (h : A.is_hermitian) (f : α → β)
-    (hf : f ∘ star = star ∘ f) :
+  (hf : function.semiconj f star star) :
   (A.map f).is_hermitian :=
-by {refine (conj_transpose_map f hf).symm.trans _, rw h.eq }
+(conj_transpose_map f hf).symm.trans $ h.eq.symm ▸ rfl
 
 @[simp] lemma is_hermitian.transpose {A : matrix n n α} (h : A.is_hermitian) :
   Aᵀ.is_hermitian :=
 by { rw [is_hermitian, conj_transpose, transpose_map], congr, exact h }
 
 @[simp] lemma is_hermitian.conj_transpose {A : matrix n n α} (h : A.is_hermitian) :
   Aᴴ.is_hermitian :=
-h.transpose.map _ rfl
+h.transpose.map _ $ λ _, rfl
 
 @[simp] lemma is_hermitian.add {A B : matrix n n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
   (A + B).is_hermitian :=