Commit 2022-01-12 07:31 c1f3f1af
View on Github →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.