Determinants of maps in the complex numbers as a vector space over ℝ

This file provides results about the determinants of maps in the complex numbers as a vector space over ℝ.

@[simp]

theorem Complex.det_conjAe : LinearMap.det (AlgEquiv.toLinearMap Complex.conjAe) = -1

The determinant of conjAe, as a linear map.

@[simp]

theorem Complex.linearEquiv_det_conjAe : LinearEquiv.det (AlgEquiv.toLinearEquiv Complex.conjAe) = -1

The determinant of conjAe, as a linear equiv.