mathlib3 documentation

analysis.inner_product_space.conformal_linear_map

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.

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.