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