# mathlibdocumentation

analysis.complex.conformal

# 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 conj is 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 conj.

## Warning #

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

theorem is_conformal_map_complex_linear {E : Type u_1} [normed_group E] [ E] [ E] [ E] {map : →L[] E} (nonzero : map 0) :
theorem is_conformal_map_complex_linear_conj {E : Type u_1} [normed_group E] [ E] [ E] [ E] {map : →L[] E} (nonzero : map 0) :
theorem is_conformal_map.is_complex_or_conj_linear {g : →L[] } (h : is_conformal_map g) :
(∃ (map : , ∃ (map : ,
theorem is_conformal_map_iff_is_complex_or_conj_linear {g : →L[] } :
((∃ (map : , ∃ (map : , g 0

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.