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 ↑conjLIE.toLinearEquiv = -1

The determinant of conjLIE, as a linear map.

@[simp]

theorem Complex.linearEquiv_det_conjLIE : LinearEquiv.det conjLIE.toLinearEquiv = -1

The determinant of conjLIE, as a linear equiv.

@[simp]

theorem Complex.reCLM_norm : ‖reCLM‖ = 1

@[simp]

theorem Complex.reCLM_eNorm : ‖reCLM‖ₑ = 1

@[deprecated Complex.reCLM_eNorm (since := "2026-11-06")]

theorem Complex.reCLM_enorm : ‖reCLM‖ₑ = 1

Alias of Complex.reCLM_eNorm.

@[simp]

theorem Complex.reCLM_nnNorm : ‖reCLM‖₊ = 1

@[deprecated Complex.reCLM_nnNorm (since := "2026-10-31")]

theorem Complex.reCLM_nnnorm : ‖reCLM‖₊ = 1

Alias of Complex.reCLM_nnNorm.

@[simp]

theorem Complex.imCLM_norm : ‖imCLM‖ = 1

@[simp]

theorem Complex.imCLM_eNorm : ‖imCLM‖ₑ = 1

@[deprecated Complex.imCLM_eNorm (since := "2026-11-06")]

theorem Complex.imCLM_enorm : ‖imCLM‖ₑ = 1

Alias of Complex.imCLM_eNorm.

@[simp]

theorem Complex.imCLM_nnNorm : ‖imCLM‖₊ = 1

@[deprecated Complex.imCLM_nnNorm (since := "2026-10-31")]

theorem Complex.imCLM_nnnorm : ‖imCLM‖₊ = 1

Alias of Complex.imCLM_nnNorm.

@[simp]

theorem Complex.conjCLE_norm : ‖↑conjCLE‖ = 1

@[simp]

theorem Complex.conjCLE_eNorm : ‖↑conjCLE‖ₑ = 1

@[deprecated Complex.conjCLE_eNorm (since := "2026-11-06")]

theorem Complex.conjCLE_enorm : ‖↑conjCLE‖ₑ = 1

Alias of Complex.conjCLE_eNorm.

@[simp]

theorem Complex.conjCLE_nnNorm : ‖↑conjCLE‖₊ = 1

@[deprecated Complex.conjCLE_nnNorm (since := "2026-10-31")]

theorem Complex.conjCLE_nnnorm : ‖↑conjCLE‖₊ = 1

Alias of Complex.conjCLE_nnNorm.

@[deprecated Complex.conjCLE_nnNorm (since := "2026-09-28")]

theorem Complex.conjCLE_nnorm : ‖↑conjCLE‖₊ = 1

Alias of Complex.conjCLE_nnNorm.

@[simp]

theorem Complex.ofRealCLM_norm : ‖ofRealCLM‖ = 1

@[simp]

theorem Complex.ofRealCLM_eNorm : ‖ofRealCLM‖ₑ = 1

@[deprecated Complex.ofRealCLM_eNorm (since := "2026-11-06")]

theorem Complex.ofRealCLM_enorm : ‖ofRealCLM‖ₑ = 1

Alias of Complex.ofRealCLM_eNorm.

@[simp]

theorem Complex.ofRealCLM_nnNorm : ‖ofRealCLM‖₊ = 1

@[deprecated Complex.ofRealCLM_nnNorm (since := "2026-10-31")]

theorem Complex.ofRealCLM_nnnorm : ‖ofRealCLM‖₊ = 1

Alias of Complex.ofRealCLM_nnNorm.