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.
theorem
inner_product_geometry.is_conformal_map.preserves_angle
{E : Type u_1}
{F : Type u_2}
[normed_add_comm_group E]
[normed_add_comm_group F]
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f' : E →L[ℝ] F}
(h : is_conformal_map f')
(u v : E) :
inner_product_geometry.angle (⇑f' u) (⇑f' v) = inner_product_geometry.angle u v
theorem
inner_product_geometry.conformal_at.preserves_angle
{E : Type u_1}
{F : Type u_2}
[normed_add_comm_group E]
[normed_add_comm_group F]
[inner_product_space ℝ E]
[inner_product_space ℝ F]
{f : E → F}
{x : E}
{f' : E →L[ℝ] F}
(h : has_fderiv_at f f' x)
(H : conformal_at f x)
(u v : E) :
inner_product_geometry.angle (⇑f' u) (⇑f' v) = inner_product_geometry.angle u v
If a real differentiable map f is conformal at a point x,
then it preserves the angles at that point.