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 conjAe.toLinearMap = -1

The determinant of conjAe, as a linear map.

@[simp]

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

The determinant of conjAe, as a linear equiv.