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 defs in analysis/convex/basic, and I don't want to import analysis.normed_space.basic there.

Estimated changes

Modified src/analysis/complex/basic.lean

deleted def complex.linear_map.im

deleted theorem complex.linear_map.im_apply

deleted def complex.linear_map.of_real

deleted theorem complex.linear_map.of_real_apply

deleted def complex.linear_map.re

deleted theorem complex.linear_map.re_apply

Modified src/data/complex/module.lean

added theorem complex.linear_map.coe_im

added theorem complex.linear_map.coe_of_real

added theorem complex.linear_map.coe_re

added def complex.linear_map.im

added def complex.linear_map.of_real

added def complex.linear_map.re