mathlib3

300e81de - feat(analysis/complex/basic): complex conjugation is a linear isometry (#6436)

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`.