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 #

Warning #

Antiholomorphic functions such as the complex conjugate are considered as conformal functions in this file.

theorem isConformalMap_conj :
IsConformalMap { toLinearEquiv := Complex.conjLIE.toLinearEquiv, continuous_toFun := , continuous_invFun := }

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.