# mathlib3documentation

analysis.normed_space.conformal_linear_map

# Conformal Linear Maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• is_conformal_map: 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
• is_conformal_map_of_subsingleton: all continuous linear maps on singleton spaces are conformal
• is_conformal_map.preserves_angle: if a continuous linear map is conformal, then it preserves all angles in the normed space

See analysis.normed_space.conformal_linear_map.inner_product for

• is_conformal_map_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 is_conformal_map {R : Type u_1} {X : Type u_2} {Y : Type u_3} [normed_field R] [ X] [ Y] (f' : X →L[R] Y) :
Prop

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

Equations
theorem is_conformal_map_id {R : Type u_1} {M : Type u_2} [normed_field R] [ M] :
theorem is_conformal_map.smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [normed_field R] [ M] [ N] {f : M →L[R] N} (hf : is_conformal_map f) {c : R} (hc : c 0) :
theorem is_conformal_map_const_smul {R : Type u_1} {M : Type u_2} [normed_field R] [ M] {c : R} (hc : c 0) :
@[protected]
theorem linear_isometry.is_conformal_map {R : Type u_1} {M : Type u_2} {N : Type u_3} [normed_field R] [ M] [ N] (f' : M →ₗᵢ[R] N) :
theorem is_conformal_map_of_subsingleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [normed_field R] [ M] [ N] [subsingleton M] (f' : M →L[R] N) :
theorem is_conformal_map.comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {G : Type u_4} [normed_field R] [ M] [ N] [ G] {f : M →L[R] N} {g : N →L[R] G} (hg : is_conformal_map g) (hf : is_conformal_map f) :
@[protected]
theorem is_conformal_map.injective {R : Type u_1} {N : Type u_3} {M' : Type u_5} [normed_field R] [ N] [ M'] {f : M' →L[R] N} (h : is_conformal_map f) :
theorem is_conformal_map.ne_zero {R : Type u_1} {N : Type u_3} {M' : Type u_5} [normed_field R] [ N] [ M'] [nontrivial M'] {f' : M' →L[R] N} (hf' : is_conformal_map f') :
f' 0