Conformal maps between complex vector spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
We prove the sufficient and necessary conditions for a real-linear map between complex vector spaces
to be conformal.
Main results #
Antiholomorphic functions such as the complex conjugate are considered as conformal functions in
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.