mathlib3 documentation


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 #

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.