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`.
mathlib3
c1f3f1af - feat(analysis/complex/basic): determinant of `conj_lie` (#11389)
