Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`.
- Loading branch information