The basic continuous linear maps associated to ℂ
#
The continuous linear maps Complex.reClm
(real part), Complex.imClm
(imaginary part),
Complex.conjCle
(conjugation), and Complex.ofRealClm
(inclusion of ℝ
) were introduced in
Analysis.Complex.Basic
. This file contains a few calculations requiring more imports:
the operator norm and (for Complex.conjCle
) the determinant.
@[simp]
The determinant of conjLie
, as a linear map.
@[simp]
The determinant of conjLie
, as a linear equiv.