mathlib documentation


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.

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.