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]

theorem Complex.det_conjLie : ↑LinearMap.det ↑Complex.conjLie.toLinearEquiv = -1

The determinant of conjLie, as a linear map.

@[simp]

theorem Complex.linearEquiv_det_conjLie : ↑LinearEquiv.det Complex.conjLie.toLinearEquiv = -1

The determinant of conjLie, as a linear equiv.

@[simp]

theorem Complex.reClm_norm : ‖Complex.reClm‖ = 1

@[simp]

theorem Complex.reClm_nnnorm : ‖Complex.reClm‖₊ = 1

@[simp]

theorem Complex.imClm_norm : ‖Complex.imClm‖ = 1

@[simp]

theorem Complex.imClm_nnnorm : ‖Complex.imClm‖₊ = 1

@[simp]

theorem Complex.conjCle_norm : ‖↑Complex.conjCle‖ = 1

@[simp]

theorem Complex.conjCle_nnorm : ‖↑Complex.conjCle‖₊ = 1

@[simp]

theorem Complex.ofRealClm_norm : ‖Complex.ofRealClm‖ = 1

@[simp]

theorem Complex.ofRealClm_nnnorm : ‖Complex.ofRealClm‖₊ = 1