Real determinants on the complex plane

The real determinant of a real-linear endomorphism of the complex plane is the two-by-two determinant of its values at 1 and I in the basis (1,I).

theorem LinearMap.det_complex (L : ℂ →ₗ[ℝ] ℂ) : LinearMap.det L = (L 1).re * (L Complex.I).im - (L Complex.I).re * (L 1).im

The real determinant of a map on the complex plane, expressed in the basis (1,I).