mathlib3 documentation

data.complex.determinant

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[simp]
theorem complex.det_conj_ae  :
⇑linear_map.det complex.conj_ae.to_linear_map = -1

The determinant of conj_ae, as a linear map.

source
@[simp]
theorem complex.linear_equiv_det_conj_ae  :
⇑linear_equiv.det complex.conj_ae.to_linear_equiv = -1

The determinant of conj_ae, as a linear equiv.