complex linear and conj linear parts

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have complex linear and complex conjugate linear parts of a (continuous) real linear map?

[Heather Macbeth]

@Yury G. Kudryashov No, but it'd be great to have. We also haven't yet implemented restrict_scalars of a conjugate-linear map to a real-linear map (should be written in more generality, of course), which is a prerequisite I think.

[Yury G. Kudryashov]

How should I call them?