Conformal Maps #
A continuous linear map between real normed spaces
ConformalAt some point
if it is real differentiable at that point and its differential is a conformal linear map.
Main definitions #
ConformalAt: the main definition of conformal maps
Conformal: maps that are conformal at every point
Main results #
- The conformality of the composition of two conformal maps, the identity map and multiplications by nonzero constants
conformalAt_iff_isConformalMap_fderiv: an equivalent definition of the conformality of a map
conformalAt_iff: an equivalent definition of the conformality of a map
ConformalAt.preserves_angle: if a map is conformal at
x, then its differential preserves all angles at
The definition of conformality in this file does NOT require the maps to be orientation-preserving. Maps such as the complex conjugate are considered to be conformal.
A function is a conformal map if and only if its differential is a conformal linear map