isConformalMap_iff_is_complex_or_conj_linear

theorem isConformalMap_iff_is_complex_or_conj_linear : ∀ {g : ℂ →L[ℝ] ℂ}, IsConformalMap g ↔ ((∃ map, ContinuousLinearMap.restrictScalars ℝ map = g) ∨ ∃ map, ContinuousLinearMap.restrictScalars ℝ map = g.comp ↑Complex.conjCLE) ∧ g ≠ 0

The theorem `isConformalMap_iff_is_complex_or_conj_linear` states that a real continuous linear map `g` on the complex plane is conformal (meaning that it's a nonzero multiple of a linear isometry) if and only if the map `g` or its conjugate is complex linear and the map `g` is nonvanishing. Concretely, the map `g` or its conjugate being complex linear is represented by the existence of a map such that when we restrict its scalars to real numbers, we get the map `g` or the composition of `g` and the complex conjugate function (represented by `Complex.conjCLE`), respectively.

More concisely: A real continuous linear map on the complex plane is conformal if and only if it is a nonvanishing complex linear map or the composition of a complex linear map and the complex conjugate function.