Documentation

Mathlib.Data.Complex.Determinant

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

The determinant of conjAe, as a linear map.

@[simp]
theorem Complex.linearEquiv_det_conjAe :
LinearEquiv.det Complex.conjAe.toLinearEquiv = -1

The determinant of conjAe, as a linear equiv.