Commit 2020-08-20 08:00 ba06edc1
View on Github →chore(data/complex/module): move linear_map.{re,im,of_real}
from analysis
(#3874)
I'm going to use these def
s in analysis/convex/basic
, and I don't
want to import analysis.normed_space.basic
there.