feat(analysis/complex/basic): determinant of conj_lie (#11389)

Add lemmas giving the determinant of `conj_lie`, as a linear map and
as a linear equiv, deduced from the corresponding lemmas for `conj_ae`
which is used to define `conj_lie`.  This completes the basic lemmas
about determinants of linear isometries of `ℂ` (which can thus be used
to talk about how those isometries affect orientations), since we also
have `linear_isometry_complex` describing all such isometries in terms
of `rotation` and `conj_lie`.

Author: jsm28

src/analysis/complex/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import data.complex.module
+import data.complex.determinant
 import data.complex.is_R_or_C
 
 /-!
@@ -142,6 +142,14 @@ def conj_lie : ℂ ≃ₗᵢ[ℝ] ℂ := ⟨conj_ae.to_linear_equiv, abs_conj⟩
 
 lemma isometry_conj : isometry (conj : ℂ → ℂ) := conj_lie.isometry
 
+/-- The determinant of `conj_lie`, as a linear map. -/
+@[simp] lemma det_conj_lie : (conj_lie.to_linear_equiv : ℂ →ₗ[ℝ] ℂ).det = -1 :=
+det_conj_ae
+
+/-- The determinant of `conj_lie`, as a linear equiv. -/
+@[simp] lemma linear_equiv_det_conj_lie : conj_lie.to_linear_equiv.det = -1 :=
+linear_equiv_det_conj_ae
+
 @[continuity] lemma continuous_conj : continuous (conj : ℂ → ℂ) := conj_lie.continuous
 
 /-- Continuous linear equiv version of the conj function, from `ℂ` to `ℂ`. -/