From 3d237db71d2e7b5153be4241c45b5dd5e76166b2 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 22 Oct 2021 15:58:26 +0000
Subject: [PATCH] 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`
---
 src/linear_algebra/matrix/determinant.lean | 20 ++++++++++++++++----
 src/ring_theory/trace.lean                 |  2 +-
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/linear_algebra/matrix/determinant.lean b/src/linear_algebra/matrix/determinant.lean
index f8b3209765491..b84aa5907ff8c 100644
--- a/src/linear_algebra/matrix/determinant.lean
+++ b/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
diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
index e3754d741e016..69e9dae1053c1 100644
--- a/src/ring_theory/trace.lean
+++ b/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 _,