Documentation

Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal

Angles and conformal maps #

This file proves that conformal maps preserve angles.

theorem InnerProductGeometry.ConformalAt.preserves_angle {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace E] [InnerProductSpace F] {f : EF} {x : E} {f' : E →L[] F} (h : HasFDerivAt f f' x) (H : ConformalAt f x) (u v : E) :
angle (f' u) (f' v) = angle u v

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