Conformal maps between complex vector spaces #
We prove the sufficient and necessary conditions for a real-linear map between complex vector spaces to be conformal.
Main results #
is_conformal_map_complex_linear: a nonzero complex linear map into an arbitrary complex normed space is conformal.
is_conformal_map_complex_linear_conj: the composition of a nonzero complex linear map with
conjis complex linear.
is_conformal_map_iff_is_complex_or_conj_linear: a real linear map between the complex plane is conformal iff it's complex linear or the composition of some complex linear map and
Antiholomorphic functions such as the complex conjugate are considered as conformal functions in this file.
A real continuous linear map on the complex plane is conformal if and only if the map or its conjugate is complex linear, and the map is nonvanishing.