Documentation

Mathlib.Analysis.Complex.OperatorNorm

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.