Theorems · Theorem · functional analysis

isConformalMap_iff

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : 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.

Defined in

Mathlib.Analysis.InnerProductSpace.ConformalLinearMap

Cited by

1 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpace