Commit 2021-02-26 07:13 300e81de

View on Github →

feat(analysis/complex/basic): complex conjugation is a linear isometry (#6436) Complex conjugation is a linear isometry (and various corollaries, eg it is a continuous linear map). Also rewrite the results that re and im are continuous linear maps, to deduce from explicit bounds rather than passing through linear_map.continuous_of_finite_dimensional.

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem complex.continuous_conj

added def complex.continuous_linear_map.conj

added theorem complex.continuous_linear_map.conj_apply

added theorem complex.continuous_linear_map.conj_coe

added theorem complex.continuous_linear_map.conj_norm

modified def complex.continuous_linear_map.im

modified def complex.continuous_linear_map.re

added theorem complex.isometry_conj

added def complex.linear_isometry.conj

Modified src/data/complex/module.lean

added theorem complex.linear_map.coe_conj

added def complex.linear_map.conj