Angles and conformal maps

This file proves that conformal maps preserve angles.

theorem InnerProductGeometry.IsConformalMap.preserves_angle {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f' : E →L[ℝ] F} (h : IsConformalMap f') (u v : E) : angle (f' u) (f' v) = angle u v

theorem InnerProductGeometry.ConformalAt.preserves_angle {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] {f : E → F} {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.