mathlib3 documentation

analysis.complex.operator_norm

The basic continuous linear maps associated to ℂ #

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

The continuous linear maps complex.re_clm (real part), complex.im_clm (imaginary part), complex.conj_cle (conjugation), and complex.of_real_clm (inclusion of ℝ) were introduced in analysis.complex.operator_norm. This file contains a few calculations requiring more imports: the operator norm and (for complex.conj_cle) the determinant.

source
@[simp]
theorem complex.det_conj_lie  :
⇑linear_map.det ↑(complex.conj_lie.to_linear_equiv) = -1

The determinant of conj_lie, as a linear map.

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

The determinant of conj_lie, as a linear equiv.

source
@[simp]
theorem complex.re_clm_norm  :
‖complex.re_clm‖ = 1
source
@[simp]
theorem complex.re_clm_nnnorm  :
‖complex.re_clm‖₊ = 1
source
@[simp]
theorem complex.im_clm_norm  :
‖complex.im_clm‖ = 1
source
@[simp]
theorem complex.im_clm_nnnorm  :
‖complex.im_clm‖₊ = 1
source
@[simp]
theorem complex.conj_cle_norm  :
‖↑complex.conj_cle‖ = 1
source
@[simp]
theorem complex.conj_cle_nnorm  :
‖↑complex.conj_cle‖₊ = 1
source
@[simp]
theorem complex.of_real_clm_norm  :
‖complex.of_real_clm‖ = 1
source
@[simp]
theorem complex.of_real_clm_nnnorm  :
‖complex.of_real_clm‖₊ = 1