Commit 2021-03-11 17:09 bd3695ac
View on Github →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.