Commit 2021-02-26 07:13 300e81deView 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
im are continuous linear maps, to deduce from explicit bounds rather than passing through