mathlib

e4a41e6f - feat(data/complex/module,data/complex/determinant): `conj_ae` matrix representation and determinant (#11337)

feat(data/complex/module,data/complex/determinant): `conj_ae` matrix representation and determinant (#11337) Add lemmas giving the matrix representation of `conj_ae` (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 (so it's actually `conj_lie` I'm interested in, but `conj_lie` is defined in terms of `conj_ae` so proving things first for `conj_ae` seems appropriate).