Conformal Maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
A continuous linear map between real normed spaces
conformal_at some point
if it is real differentiable at that point and its differential
Main definitions #
Main results #
- The conformality of the composition of two conformal maps, the identity map
and multiplications by nonzero constants
conformal_at_iff_is_conformal_map_fderiv: an equivalent definition of the conformality of a map
conformal_at.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.
f is said to be conformal if it has a conformal differential
A function is a conformal map if and only if its differential is a conformal linear map
f is conformal if it's conformal at every point.