mathlib3

bd3695ac - feat(data/complex/is_R_or_C): add linear maps for is_R_or_C.re, im, conj and of_real (#6621)

feat(data/complex/is_R_or_C): add linear maps for is_R_or_C.re, im, conj and of_real (#6621) Add continuous linear maps and linear isometries (when applicable) for the following `is_R_or_C` functions: `re`, `im`, `conj` and `of_real`. Rename the existing continuous linear maps defined in complex.basic to adopt the naming convention of is_R_or_C. Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>