mathlib3

83b03557 - feat(analysis/complex/isometry): `rotation` matrix representation and determinant (#11339)

feat(analysis/complex/isometry): `rotation` matrix representation and determinant (#11339) Add lemmas giving the matrix representation of `rotation` (with respect to `basis_one_I`), and its determinant (both as a linear map and as a linear equiv). This is preparation for doing things about how isometries affect orientations.