mathlib3 documentation

geometry.euclidean.angle.unoriented.conformal

Angles and conformal maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves that conformal maps preserve angles.

If a real differentiable map f is conformal at a point x, then it preserves the angles at that point.