feat(linear_algebra/matrix/determinant): det_conj_transpose (#9879)

Also:
* Makes the arguments of `ring_hom.map_det` and `alg_hom.map_det` explicit, and removes them from the `matrix` namespace to enable dot notation.
* Adds `ring_equiv.map_det` and `alg_equiv.map_det`

Author: eric-wieser

src/linear_algebra/matrix/determinant.lean

@@ -263,17 +263,29 @@ section hom_map
 
 variables {S : Type w} [comm_ring S]
 
-lemma ring_hom.map_det {M : matrix n n R} {f : R →+* S} :
+lemma _root_.ring_hom.map_det (f : R →+* S) (M : matrix n n R) :
   f M.det = matrix.det (f.map_matrix M) :=
 by simp [matrix.det_apply', f.map_sum, f.map_prod]
 
-lemma alg_hom.map_det [algebra R S] {T : Type z} [comm_ring T] [algebra R T]
-  {M : matrix n n S} {f : S →ₐ[R] T} :
+lemma _root_.ring_equiv.map_det (f : R ≃+* S) (M : matrix n n R) :
+  f M.det = matrix.det (f.map_matrix M) :=
+f.to_ring_hom.map_det _
+
+lemma _root_.alg_hom.map_det [algebra R S] {T : Type z} [comm_ring T] [algebra R T]
+  (f : S →ₐ[R] T) (M : matrix n n S) :
   f M.det = matrix.det ((f : S →+* T).map_matrix M) :=
-by rw [← alg_hom.coe_to_ring_hom, ring_hom.map_det]
+f.to_ring_hom.map_det _
+
+lemma _root_.alg_equiv.map_det [algebra R S] {T : Type z} [comm_ring T] [algebra R T]
+  (f : S ≃ₐ[R] T) (M : matrix n n S) :
+  f M.det = matrix.det ((f : S →+* T).map_matrix M) :=
+f.to_alg_hom.map_det _
 
 end hom_map
 
+@[simp] lemma det_conj_transpose [star_ring R] (M : matrix m m R) : det (Mᴴ) = star (det M) :=
+((star_ring_aut : ring_aut R).map_det _).symm.trans $ congr_arg star M.det_transpose
+
 section det_zero
 /-!
 ### `det_zero` section

src/ring_theory/trace.lean

@@ -359,7 +359,7 @@ begin
     vandermonde (λ i, e.symm i pb.gen),
   calc algebra_map K (algebraic_closure _) (bilin_form.to_matrix pb.basis (trace_form K L)).det
       = det ((algebra_map K _).map_matrix $
-              bilin_form.to_matrix pb.basis (trace_form K L)) : ring_hom.map_det
+              bilin_form.to_matrix pb.basis (trace_form K L)) : ring_hom.map_det _ _
   ... = det (Mᵀ ⬝ M) : _
   ... = det M * det M : by rw [det_mul, det_transpose]
   ... ≠ 0 : mt mul_self_eq_zero.mp _,