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.

@[simp]

The determinant of conj_lie, as a linear map.

@[simp]

The determinant of conj_lie, as a linear equiv.