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 isConformalMap_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] (f : E →L[ℝ] F) : IsConformalMap f ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (u v : E), inner (f u) (f v) = c * 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.