mathlib documentation

analysis.inner_product_space.conformal_linear_map

Conformal maps between inner product spaces #

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} [inner_product_space E] [inner_product_space F] (f' : E →L[] F) :
is_conformal_map f' ∃ (c : ), 0 < c ∀ (u v : E), inner (f' u) (f' v) = c * inner u v