Conformal maps between inner product spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In an inner product space, a map is conformal iff it preserves inner products up to a scalar factor.
theorem
is_conformal_map_iff
{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) :
is_conformal_map f ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (u v : E), has_inner.inner (⇑f u) (⇑f v) = c * has_inner.inner u v
A map between two inner product spaces is a conformal map if and only if it preserves inner
products up to a scalar factor, i.e., there exists a positive c : ℝ such that ⟪f u, f v⟫ = c * ⟪u, v⟫ for all u, v.