feat(linear_algebra/determinant): linear_equiv.det_mul_det_symm (#10635)

Add lemmas that the determinants of a `linear_equiv` and its
inverse multiply to 1.  There are a few other lemmas involving
determinants and `linear_equiv`, but apparently not this one.

src/linear_algebra/determinant.lean

@@ -268,6 +268,16 @@ end
 
 end linear_map
 
+/-- The determinants of a `linear_equiv` and its inverse multiply to 1. -/
+@[simp] lemma linear_equiv.det_mul_det_symm {A : Type*} [comm_ring A] [is_domain A] [module A M]
+  (f : M ≃ₗ[A] M) : (f : M →ₗ[A] M).det * (f.symm : M →ₗ[A] M).det = 1 :=
+by simp [←linear_map.det_comp]
+
+/-- The determinants of a `linear_equiv` and its inverse multiply to 1. -/
+@[simp] lemma linear_equiv.det_symm_mul_det {A : Type*} [comm_ring A] [is_domain A] [module A M]
+  (f : M ≃ₗ[A] M) : (f.symm : M →ₗ[A] M).det * (f : M →ₗ[A] M).det = 1 :=
+by simp [←linear_map.det_comp]
+
 -- Cannot be stated using `linear_map.det` because `f` is not an endomorphism.
 lemma linear_equiv.is_unit_det (f : M ≃ₗ[R] M') (v : basis ι R M) (v' : basis ι R M') :
   is_unit (linear_map.to_matrix v v' f).det :=