# Documentation

Mathlib.Analysis.NormedSpace.ConformalLinearMap

# Conformal Linear Maps #

A continuous linear map between R-normed spaces X and Y IsConformalMap if it is a nonzero multiple of a linear isometry.

## Main definitions #

• IsConformalMap: the main definition of conformal linear maps

## Main results #

• The conformality of the composition of two conformal linear maps, the identity map and multiplications by nonzero constants as continuous linear maps
• isConformalMap_of_subsingleton: all continuous linear maps on singleton spaces are conformal

See Analysis.InnerProductSpace.ConformalLinearMap for

• isConformalMap_iff: a map between inner product spaces is conformal iff it preserves inner products up to a fixed scalar factor.

conformal

## Warning #

The definition of conformality in this file does NOT require the maps to be orientation-preserving.

def IsConformalMap {R : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] (f' : X →L[R] Y) :

A continuous linear map f' is said to be conformal if it's a nonzero multiple of a linear isometry.

Instances For
theorem isConformalMap_id {R : Type u_1} {M : Type u_2} [] [] :
theorem IsConformalMap.smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] {f : M →L[R] N} (hf : ) {c : R} (hc : c 0) :
theorem isConformalMap_const_smul {R : Type u_1} {M : Type u_2} [] [] {c : R} (hc : c 0) :
theorem LinearIsometry.isConformalMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] (f' : M →ₗᵢ[R] N) :
theorem isConformalMap_of_subsingleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [] [] [] [] (f' : M →L[R] N) :
theorem IsConformalMap.comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {G : Type u_4} [] [] [] [] {f : M →L[R] N} {g : N →L[R] G} (hg : ) (hf : ) :
theorem IsConformalMap.injective {R : Type u_1} {N : Type u_3} {M' : Type u_5} [] [] [] [NormedSpace R M'] {f : M' →L[R] N} (h : ) :
theorem IsConformalMap.ne_zero {R : Type u_1} {N : Type u_3} {M' : Type u_5} [] [] [] [NormedSpace R M'] [] {f' : M' →L[R] N} (hf' : ) :
f' 0