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 : E) (v : E) :

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